What mathematicians should know about the Lean Theorem Prover: reliability & AI

This piece explains how computer-checked formal proofs and the Lean theorem prover have moved from niche projects to mainstream mathematical tools. Lean, developed by Leo de Moura and supported by a massive community-maintained mathlib (roughly 300,000 theorems, 100,000 definitions, 2.5M lines of code), has been used to formalize landmark results and, in 2025-2026, to autoformalize large swathes of existing mathematics. Multiple high-profile autoformalizations are described: quasi-autoformalization of the prime number theorem, large parts of Munkres’s topology, sphere-packing proofs in 8 and 24 dimensions, Meta’s ATLAS of textbooks, and massive projects claiming formal versions of Fermat’s Last Theorem and Navier-Stokes blowup. These projects generated enormous codebases (reports range up to millions of lines) and mark autoformalization as a practical reality.

The post examines reliability: Lean is built on CIC type theory, which can be translated to and from ZFC, and combines a programming language with a mathematical language whose proofs are elaborated and checked by a C++ kernel. Kernel soundness is critical because a kernel bug can validate false proofs; several such soundness bugs surfaced in the summer of 2026 (some enabling illicit proofs), but were rapidly fixed and mathlib rechecked. The author stresses that Lean-verified statements still require human audits for statement fidelity and recommends tools and scrutiny to ensure definitions and axioms match intended mathematics. Detection of recent bugs by AI and security researchers is framed as a salutary stress test rather than a fatal flaw.