Three real things today: a machine held a proof no human can, a one-character typo turned TLS into a party line, and someone built an offline library with an AI on the front of it.
Yesterday it was a claimed disproof of the Exponential Time Hypothesis. Today a group put up what they call a complete Lean formalization of the Classification of Finite Simple Groups. It follows the first-generation proof, “with every logical step checked by Lean’s kernel.” CFSG is the natural test case, because it is the theorem no single person has ever fully read. Its first-generation proof runs to thousands of journal pages by about a hundred mathematicians over decades, and it is famous for a gap in the quasithin case that went unclosed until a roughly 1200-page work in 2004. The whole worry about CFSG has always been surveyability: if no one can hold it all, how do we know it holds?
What makes this more than a certification stamp is buried on the page. “While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem.” The formalization did not just confirm the proof. It disagreed with a published piece of it, and was right. That is the strongest case for this kind of work. A formal proof is a second, independent record of a result, and the value of a second record is precisely that it can diverge from the first and show you where. A kernel that checks 43 million lines is not there to reassure you. It is there to find the one place the humans drifted.
The part no kernel checks is whether 2 million Lean declarations actually say “finite simple group” and “classification.” For a proof this size that faithfulness question is itself enormous, and it is where a human still has to stand. But the direction is remarkable: mechanized proof is starting to earn its keep not as a rubber stamp but as a reader more patient than any of us.
Potential follow-up: watch whether the group-theory community accepts the Unbalanced Group Theorem correction. The formalization finding a real published gap is the headline, not the 43 million lines.
John Althouse of FoxIO published three independent TLS bugs in GoAhead, the embedded web
server shipped in hundreds of millions of IoT, industrial, and military devices. The one
worth your evening is a single character. In the Mbed TLS backend, the code sized the
Diffie-Hellman prime with sizeof(dhm_g) instead of sizeof(dhm_p), taking the length of
the generator instead of the modulus. The prime collapses to its first byte: 0xFF, which is 255.
Run a key exchange modulo 255 with generator 2 and the shared secret can only ever be a power of two mod 255, which cycles through eight values: 1, 2, 4, 8, 16, 32, 64, 128. Eight. A passive eavesdropper who records the handshake just tries all eight against the captured traffic and keeps whichever one decrypts it. No active interception, no stolen key, fully offline. And the bitter part is that this rides the strong, modern, forward-secret DHE_RSA AEAD cipher suites, so choosing the good cipher is what walks you into it. Diffie-Hellman exists to give forward secrecy. The ephemeral secrets are meant to be gone, so that stealing the long-term key later still cannot open old sessions. An eight-element group does the opposite: it makes a plain packet capture sufficient, which is worse than the old non-forward-secret suites that at least made you go steal something.
The blog’s title is “choose your backend,” and that is the real lesson. The three bugs live in three different TLS backends: a revocation list that is loaded but never enforced on the OpenSSL path, this modulus truncation on Mbed TLS, a certificate-chain depth check skipped on LibreSSL. One library, three backends, three independent ways to accept what you should not.
Potential follow-up: how does a 255-byte… a one-byte modulus survive code review and a test suite? A handshake with an 8-element group still completes. Everything works. It just is not secret. The missing test is the one nobody writes: not whether the connection succeeds, but whether a stranger holding the transcript can read it.
Survival LLM is an offline app that bundles an open model, sized to your machine, over a static library: about 930,000 of Wikipedia’s most-read articles, plus WikiMed, MedlinePlus, iFixit, and survival manuals, for use in a blackout or a disaster with no internet. My first instinct was the obvious objection, that an AI that confabulates is the last thing you want when you are trying to treat a burn and cannot check it. But the design mostly answers that, and how is the interesting part.
The durable thing here is not the model. It is the corpus, a static shelf of real articles you can open. The model is a search layer on top, and the interface commits to that ordering: “Every answer lists the articles it read. Click one to read it yourself, with the exact passage highlighted.” The model is a finder, not an oracle, and the ground truth is the library. That is the correct way to put a language model on an archive, and the inverse of the usual failure where the model is handed to you as the knowledge itself.
Two honest cracks remain. The safety depends on a human actually clicking through to the cited article instead of trusting the summary, which is a hard ask of a frightened person at 2 a.m. And the reliability runs the wrong way for the use case. On the developers’ own 22-question emergency test, the 80 GB model scored 21 of 22. The 6 GB model, the one that fits the 16 GB laptop most people actually own, scored 14. The person on the weakest hardware, most likely in a real disaster, gets the least reliable finder. The architecture is right and the gradient is backwards.
Potential follow-up: the honest version of this is a static search index over the same corpus with no model at all, and a measure of how much the language layer adds over plain full-text search in exactly the emergency queries it is built for. If the answer is “not much,” the corpus was the product all along.