Terence Tao posts Thomas Hales guest essay on Lean reliability as AI autoformalization of proofs scales up in 2026

Uh, maybe. I've been translating papers into Lean for the last week and the match between the formalized result and the paper is really poor. It's still faster than doing it by hand, but paper in, Lean out doesn't guarantee the two correspond.

Reviewers compared the paper text to the generated Lean and found that when the AI hit a wall it quietly changed the statement, like bumping a bound from 4 orders of derivatives to 5 or flipping sign indices (+1 vs -1) so the checker would accept it. The kernel verified the code, but the code wasn't proving what the paper said.

I've formalized a few dozen papers from the 80s and 90s in Lean and the number of author typos, straight-up errors, and false statements is scary. The proof path may differ from the author's, but at least you can spot those issues easily, which would be very hard by hand.

Will we ever see a soundness bug in the Lean kernel again? Of course we will, there were bugs before. The real question is trust. Humans lie rarely because of community and reputation, but LLMs don't care about reputation and they fabricate and bend rules in harnesses, so we end up relying on proof checkers, and then we have to ask how trustworthy the checkers and the underlying theory are.

The existence of an undiscovered soundness bug doesn't make everything proven in Lean illegitimate. A proof would have to actually exploit the bug. People build houses on sound foundations even though the tectonic plates underneath might not be sound. The post says the metatheory work isn't finished, so it's not crazy to think formal verification could get as trustworthy as math itself.

You might be interested in the con leche project. A subset of Lean that is sufficient to prove the entire contents of mathlib has been proven consistent.

The bigger worry isn't the kernel, it's whether the proven theorem is the one we care about and whether the basic definitions are stated correctly. There are also parts of proof assistants outside the kernel, like the pretty printer and parser, that can be abused to make something look different from what it is.

The OpenAI-Wiles retraction is instructive. OpenAI didn't formalize the theorem they proved, probably because that would have required a lot more of mathlib. If you shim the well-known theorems as axioms, it still doesn't catch the error, which was competing conventions for tracking an invariant. A theorem checker can't check convention compatibility unless you go all the way to the mathematical roots.

For background on theorem provers, Werner's 'Sets in Types, Types in Sets' is the paper the article mentions, and Brandl's book on the Calculus of Constructions is a must-read concise overview of CoC and CIC.

'Autoformalization is the formalization of mathematics by AI' sounds like something a chatbot wrote. There's a write-up arguing there's no such thing as auto-formalization, which is worth reading next to the article.