Mathematicians Assess Lean Theorem Prover Reliability Amid AI-Driven Autoformalization Surge

The Rise of AI Autoformalization

Mathematicians are witnessing a shift toward autoformalization, where AI converts natural language proofs into machine-checkable code for the Lean theorem prover. This transition accelerated in 2025–2026, with major milestones including:

• Anthropic announced the autoformalization of Fermat’s Last Theorem in September 2026, generating 13 million lines of Lean code in 11 days.
• OpenAI released a formalization of Navier-Stokes blowup with forcing alongside Lean code in September 2026.
• Meta/Facebook Research’s ATLAS project autoformalized significant portions of 26 math textbooks by May 2026.
• The Mathematics Autoformalization Project (MAP) launched in September 2026 with a goal to translate all known mathematics into code, targeting a scale of 1 trillion lines.

Reliability Concerns and Soundness Bugs

Despite the productivity gains, the reliability of the underlying verification infrastructure remains a critical concern. The article details a period termed the “Summer of Soundness Bugs” (July–August 2026), during which several critical flaws were discovered in Lean’s kernel. These bugs, found by security researchers using frontier AI models, allowed for the generation of illicit disproofs (e.g., for the Collatz conjecture) and short invalid proofs (e.g., for the Kepler conjecture). All identified bugs were quickly patched, and the mathlib library (containing ~300,000 theorems and 2.5 million lines of code) was re-verified.

Unresolved Type-Theoretic Foundations

A central argument by authors Thomas Hales and Terence Tao is that Lean’s theoretical foundations are not yet fully understood or proven consistent. Key issues include:

• Undecidable Definitional Equality: Mario Carneiro proved that determining definitional equality in Lean is undecidable, meaning the system may fail to recognize certain equivalent terms.
• Missing Relative Consistency Proofs: As of October 2026, there is no complete, publicly documented proof that Lean’s abstract type theory is logically consistent relative to set theory. While the Con-Leche project (a verified Lean kernel using set-theoretic semantics) offers a related consistency guarantee, it does not fully cover Lean’s native type theory.
• Unproven Conjectures: Fundamental properties like Unique typing, Pi-injectivity, and the modified Church-Rosser property remain unproven conjectures.

Trust in AI-Generated Verification

The authors invoke Ken Thompson’s “Reflections on Trusting Trust” to warn against blind faith in AI-generated verification tools. They argue that if AI systems are used to sweep for bugs or generate kernels, there is a risk of hidden backdoors or obscure soundness flaws that human audits might miss. The delegation of foundational research to AI without rigorous human oversight is identified as a significant risk to the integrity of formalized mathematics.