Lean Theorem Prover Faces Reliability Questions as AI Autoformalization Advances

Formalization and autoformalization

Lean has become the most popular theorem prover among mathematicians, according to a guest post by mathematician Thomas Hales. It was developed by Leo de Moura in 2013 while at Microsoft, which later made the software open-source. Lean is based on type theory, in particular a dialect called the calculus of inductive constructions. Its community library mathlib, started in 2017, now contains nearly 300,000 theorems, over 100,000 definitions, 2.5 million lines of code, and more than 700 contributors. Any theorem in mathlib can be cited in further proofs instead of being reproved.

Autoformalization, in which AI reads a paper and outputs a formal proof, became a practical reality in 2026. Milestones include a quasi-autoformalization of the prime number theorem by Math Inc. in September 2025, a formalization of large parts of Munkres's topology textbook, the sphere-packing problem in 24 dimensions, Anthropic's autoformalization of Fermat's Last Theorem on September 4, which generated 13 million lines of Lean in 11 days, and OpenAI's Navier-Stokes blowup formalization announced on September 8.

Design and reliability model

Lean combines a general-purpose programming language with a mathematical language for definitions, theorem statements, and proof scripts. Proof scripts are parsed, elaborated, and checked by the Lean kernel, a few thousand lines of C++ code. The post stresses that Lean proofs should never be believed until checked by the kernel, and that a separate human audit is needed to confirm statement fidelity, that the verified theorem is the theorem mathematicians actually intend.

The summer of soundness bugs

A soundness bug is a kernel bug that permits a proof of "False" and therefore of any proposition. Several such bugs were uncovered in Lean in July and August 2026, in what is now called the Summer of Soundness Bugs. One bug produced an illicit disproof of the Collatz conjecture, and another a short illicit proof of the Kepler conjecture. All were quickly repaired, and mathlib has been verified by the repaired kernel.

Proposals and open problems

Three responses are discussed. First, write additional Lean kernels and cross-check proofs; about 25 kernels exist, and the Navier-Stokes formalization has been confirmed by more than a dozen proof-checkers. Second, formally verify the kernel, as Joachim Breitner did with Con-Leche, a verified Lean kernel whose consistency proof was generated with Claude and has checked mathlib. Third, deepen theoretical understanding of Lean's type theory, where unique typing, Pi-injectivity, a modified Church-Rosser property, and a complete public relative-consistency proof remain open. The post closes by citing Ken Thompson's "Reflections on Trusting Trust" and warns that blind trust in systems such as Lean is no longer possible.

Sources: terrytao.wordpress.com