Tram cong nghe AI
The Lean theorem prover has become the main tool mathematicians use to check proofs by computer, and in 2026 AI started writing those proofs at huge scale. In a guest post on Terence Tao’s blog on October 9, 2026, mathematician Thomas Hales describes how AI turned Fermat’s Last Theorem into 13 million lines of Lean in 11 days. He also describes the “Summer of Soundness Bugs,” when AI found flaws that let Lean accept false proofs. His conclusion: we cannot put blind trust in Lean, and humans still need to check the work.
Key Takeaways
- Published: October 9, 2026, a guest post by Thomas Hales on Terence Tao’s blog.
- Scale: Anthropic’s autoformalization of Fermat’s Last Theorem, announced September 4, 2026, generated 13 million lines of Lean in 11 days.
- The scare: several soundness bugs were found in Lean in July and August 2026. One led to a false “disproof” of the Collatz conjecture.
- The twist: the bugs were found by frontier AI used by security researchers, not by attackers. All were quickly fixed.
- The fixes: cross-checking with many kernels, formally verifying the kernel, and strengthening Lean’s underlying theory.
- The rule: a Lean proof should be checked by the kernel and audited by a human before it is accepted.
What Is the Lean Theorem Prover?
Lean is a proof assistant: software that checks a mathematical proof step by step, down to the basic rules of logic. Hales calls such a fully checked proof a formal proof.
Leo de Moura developed Lean in 2013 while at Microsoft, and Microsoft made it open source. Among mathematicians, it is now the most popular proof assistant.
Lean’s math library, mathlib, is huge. According to the post, it holds nearly 300,000 theorems, over 100,000 definitions and 2.5 million lines of code from over 700 contributors. Any result in mathlib can be reused to prove new theorems.
The most important part of Lean is the kernel, several thousand lines of C++ that give the final verdict on every proof. If the kernel has a bug, Lean might accept a proof that is wrong.
How AI Changed Lean: Autoformalization
Autoformalization means AI reads a math paper and writes the formal proof in Lean or another proof assistant. Hales says it “has become a practical reality in 2026.”
For comparison, the formal proof of the Kepler conjecture, done by humans, took about 20 work-years and about 500,000 lines of proof scripts.
| Date | Milestone (as described in the post) |
|---|---|
| Sep 2025 | Math Inc. produced a “quasi-autoformalization” of the prime number theorem, with human help when the AI got stuck |
| Jan 2026 | J. Urban autoformalized large parts of Munkres’s topology textbook: “130k lines of formal topology in two weeks” |
| Mar 2026 | Math Inc. autoformalized sphere packing in 24 dimensions, about 500K lines, later pruned to about 200K |
| May 2026 | Meta’s ATLAS project autoformalized large parts of 26 math textbooks |
| Sep 4, 2026 | Anthropic announced the autoformalization of Fermat’s Last Theorem: 13 million lines of Lean in 11 days |
| Sep 8, 2026 | OpenAI’s Navier-Stokes blowup announcement came with a Lean autoformalization |
| Sep 8, 2026 | Jared Lichtman launched MAP, which aims to translate “all known math into formal code” |
The Summer of Lean Soundness Bugs
A soundness bug is the worst bug a proof assistant can have. It lets you prove “False,” and from that you can prove anything.
Lean 4 came out in September 2023. Two soundness bugs were fixed before release, and another was reported in May 2025. Then, in Hales’s words, “all hell broke loose” in 2026. Several soundness bugs were found in July and August:
- One bug led to an illicit disproof of the Collatz conjecture.
- Another produced a short illicit proof of the Kepler conjecture, which is how Hales learned of the problem.
Hales argues this was good news. The bugs were found “by frontier model AI in the hands of security researchers interested in reliable kernels, not by black-hat hackers.” Ramana Kumar found the Collatz bug. Dan Selsam at OpenAI used an AI specialized in cybersecurity to find others, until “the internal AI reported it could not find additional issues.” All the bugs were quickly repaired, and mathlib was checked again with the fixed kernel.
3 Ways to Make the Lean Theorem Prover More Reliable
This is the part the video promised. Hales discusses three approaches.
1. Cross-check proofs with many Lean kernels
About 25 independent kernels for Lean exist, listed in the “Lean Kernel Arena.” The Navier-Stokes formalization has already been confirmed by more than a dozen proof checkers.
Limit: cross-checking does not remove all doubt. The Collatz bug slipped past an out-of-date kernel called Nanoda, which had its own unrelated bug. Hales suggests running kernels written in different languages on different hardware, and ideally a “clean-room” kernel written without looking at Lean’s source code.
2. Formally verify the kernel itself
The goal is a formal proof that the kernel has no soundness bug. Gödel’s second incompleteness theorem means the best possible result is a relative consistency proof: if a certain system is consistent, so is Lean.
The big milestone came on September 10, 2026. Joachim Breitner released Con-Leche, a Lean checker with a formal consistency proof, with code and proofs generated by Claude. Con-Leche has checked mathlib, and its consistency proof has been checked by more than a dozen other proof checkers. Hales calls it “one of the most important milestones in Lean’s history.”
3. Strengthen the theory behind Lean
Lean is based on a version of type theory called the calculus of inductive constructions. Hales says the theory behind it is not as solid as it should be:
- The founding document, Mario Carneiro’s 2019 thesis, contained an error and targets the older Lean 3.
- Basic properties such as “unique typing” are still unproven.
- As of October 2026, Hales knows of no complete, public proof that Lean’s abstract type theory is consistent relative to set theory.
He supports Carneiro’s call for more type theorists to work on Lean.
Why Humans Still Need to Check AI Proofs
Even a perfect kernel only proves that the Lean code is valid. A human still has to confirm that the Lean statement means what we think it means. Hales calls this checking statement fidelity, and says it is “massively easier than checking the proof itself.” For Navier-Stokes, for example, a person should check that the Lean statement matches the official Millennium Prize problem.
Hales ends with a warning based on Ken Thompson’s “Reflections on Trusting Trust.” What if an AI left a hidden soundness bug in Lean during the 2026 bug sweep? His view is that relying on AI for this foundational work “is dangerous unless carefully audited by humans.”
Is the Lean Theorem Prover Reliable Enough?
Strengths
- Kernel checking catches errors a human reviewer would miss.
- Bugs found in 2026 were fixed quickly, and mathlib was rechecked.
- Many independent kernels and the verified Con-Leche checker add layers of safety.
Weaknesses
- Soundness bugs have happened, and different kernels can share defects.
- Lean’s theoretical foundations still have open questions.
- AI-generated proofs can run to millions of lines, far too much for humans to read.
Verdict: Lean is much more reliable than unchecked proofs, but not infallible. Treat any AI-made Lean proof as “kernel-checked plus human-audited,” never as automatically true.
Lean Theorem Prover FAQ
What is the Lean theorem prover?
Lean is open-source software that checks mathematical proofs down to the rules of logic. It was created by Leo de Moura at Microsoft in 2013.
What is autoformalization?
It is AI turning a written math proof into a formal proof that Lean or another proof assistant can check.
What was the Summer of Soundness Bugs?
In July and August 2026, several bugs were found in Lean’s kernel that let it accept false proofs, including a false disproof of the Collatz conjecture. All were fixed quickly.
Who found the Lean soundness bugs?
Security researchers using frontier AI, including Ramana Kumar and Dan Selsam at OpenAI.
What is Con-Leche?
A Lean checker by Joachim Breitner with a formal consistency proof, generated with Claude and released on September 10, 2026.
Sources
- Thomas Hales, “What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI,” guest post on Terence Tao’s blog: https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/
Last updated: October 13, 2026
