Thomas Hales · 2026-10-09 · notable
Thomas Hales — Lean proofs need more scrutiny as AI writes them at scale
Thomas Hales, who led the formal proof of the Kepler conjecture, argues on Terence Tao's blog that the Lean proof assistant needs far more scrutiny now that AI writes formal proofs at scale and has already found soundness bugs in it.
A proof checked by Lean is only as trustworthy as Lean itself, and AI is now writing millions of lines of it.
What is it?
"What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI" is a guest post by Thomas Hales on Terence Tao's blog. Hales writes that "we absolutely cannot put blind trust in systems such as Lean," even though Lean is the most popular proof assistant among mathematicians. He lists 2026's AI autoformalization results, from sphere packing to Anthropic's 13-million-line Fermat's Last Theorem proof, as the reason the question is now urgent.
How does it work?
The trusted core of Lean is a kernel of several thousand lines of C++; a soundness bug there would let a false proof pass. Hales recounts the "Summer of Soundness Bugs" in 2026, when security researchers using frontier AI found several such bugs, one of which allowed an illicit Collatz disproof; all were reportedly fixed. He proposes three defences: cross-checking with independent kernels (about 25 exist), formally verifying the kernel, as Joachim Breitner's Con-Leche checker does, and finishing the missing theory, since no complete public relative-consistency proof of Lean's type theory exists yet.
Why does it matter?
Labs now publish huge Lean proofs as evidence that their models did real mathematics, so the reliability of the checker carries the whole claim. Hales warns that the same AI that finds bugs could also plant a backdoor soundness bug humans miss, and concludes that foundational work handed to AI is "dangerous unless carefully audited by humans." The post reached 168 points on Hacker News.
Who is it for?
mathematicians, formal-methods engineers and anyone citing AI-made Lean proofs