Mathematician Thomas Hales assesses Lean's reliability and the rise of AI autoformalization

A guest essay by mathematician Thomas Hales, published on Terence Tao's blog and surfaced on Hacker News, sets out what working mathematicians should understand about the Lean theorem prover at a moment when AI is generating formal proofs at a pace no human team could match. Hales frames the stakes at the outset: what he values in mathematics is its consistency and its reliability in support of science and civilization. In an editorial note, Tao adds that the essay itself was converted from another file format using AI.

A year of autoformalization milestones

Hales dates the shift to late spring and summer of 2025, when researchers grew increasingly confident that autoformalization — AI reading a paper and emitting a formal proof in Lean or another proof assistant — had become practical. His timeline, as laid out in the essay:

• September 2025: Math Inc. produces a quasi-autoformalization of the prime number theorem, with humans stepping in whenever the AI got stuck.
• January 2026: J. Urban posts an arXiv preprint describing 130,000 lines of formal topology produced in two weeks, covering large parts of Munkres's topology textbook in a set-theory-based proof assistant.
• March 2026: Math Inc. autoformalizes the 24-dimensional sphere-packing result of Viazovska and her collaborators, about a week after announcing the 8-dimensional case, generating roughly 500,000 lines of code later pruned to around 200,000.
• May 2026: a group at Meta formalizes large parts of 26 mathematics textbooks in a project called ATLAS.
• September 4: Anthropic announces an autoformalization of Fermat's Last Theorem, 13 million lines of Lean produced in 11 days.
• September 8: OpenAI announces a forced-blowup result for Navier-Stokes together with a Lean formalization, and Jared Lichtman launches MAP, the Mathematics Autoformalization Project, which aims to translate "all known math into formal code."

The contrast with the pre-AI era is stark: the hand-built formal proof of the Kepler conjecture consumed roughly 20 human work-years and some 500,000 lines of proof scripts. Hales also cites Urban's January prediction that formalization "may become quite easy and ubiquitous in 2026," and Jesse Han's view, relayed by IEEE Spectrum, that commonplace large-scale formalization marks a revolutionary transformation of mathematics. Formalizations of sphere packing in 8 and 24 dimensions, Navier-Stokes and Fermat's Last Theorem were all completed this year, joining earlier landmarks such as the four-color theorem, the Feit-Thompson odd-order theorem, sphere eversion and Kepler's conjecture.

Lean and mathlib

Among mathematicians, Lean is the most popular proof assistant, ahead of systems such as Isabelle, HOL Light, Coq (renamed Rocq), Metamath and Mizar, according to the essay. Lean was introduced by Leo de Moura at Microsoft in 2013 and, to the community's benefit, open-sourced. Kevin Hartnett's history of the project, "The Proof in the Code," names Jeremy Avigad as Lean's first user; in 2017 Avigad's graduate student Mario Carneiro, working with Johannes Hölzl, split the mathematical library mathlib out of the core library. Mathlib now contains nearly 300,000 theorems and over 100,000 definitions across 2.5 million lines of code, with more than 700 contributors, and lets a proof cite an existing result such as the Cauchy-Schwarz inequality rather than re-derive it.

Is Lean reliable?

The essay's central question is whether Lean can carry the reliability that mathematics demands. Lean is built on a dialect of type theory called the calculus of inductive constructions. Hales recounts how Russell's 1901 paradox provoked a foundational crisis, answered along two paths: Zermelo's set-theoretic axioms, which disallow unsafe sets, and Russell's type theory, which turns paradoxical constructions into syntax errors. For mathematicians reared on set theory, Hales points to B. Werner's 1997 paper "Sets in Types, Types in Sets," which shows that ZFC can be encoded into CIC and that a dialect of CIC can be encoded back into ZFC augmented with a hierarchy of inaccessible cardinals. His simplifying picture is that types behave like disjoint sets: the natural number 2 and the real number 2.0 inhabit different types, connected by an explicit coercion. He also stresses that Lean is simultaneously a general-purpose programming language whose ordinary programs compile and run, and that its programming and mathematical languages are not independent entities.

Why it matters

Hales's argument is that mathematics earns its authority from consistency and reliability, and AI is about to flood the field with machine-generated proofs whose only referee is a proof assistant. That makes foundational questions about Lean newly urgent: if autoformalization becomes easy and ubiquitous, a theorem's certificate of correctness will increasingly amount to the prover having accepted it, and mathematicians need to know precisely what that guarantee rests on. With ventures like MAP talking in terms of a trillion lines of formal code, the community's understanding of the verifier itself becomes part of the trust chain behind every result.