Thomas Hales on Lean: AI autoformalization is practical, soundness bugs fixed

Thomas Hales wrote a guest post, signed by the host as 'T.', for mathematicians who want to understand the Lean theorem prover, how reliable it is, and what AI changes. An editor's note says the post was written in a different file format and converted using AI.

Hales starts from what a formal proof is: a proof exhaustively checked down to the foundations of mathematics and the rules of logic, in practice by software. He lists formalized results (the four-color theorem, the Feit-Thompson theorem, the Kepler conjecture, sphere eversion, sphere packing in 8 and 24 dimensions, Navier-Stokes forced blowup, Fermat's Last Theorem) and says the last three projects were completed this year. Among proof assistants (Automath, HOL Light, Isabelle, Coq, now renamed Rocq, Metamath, Mizar, Lean) he says Lean is the most popular among mathematicians. Leo de Moura developed and introduced Lean in 2013 while at Microsoft and persuaded Microsoft to open-source it. Jeremy Avigad, now director of Carnegie Mellon's new NSF institute ICARM, was its first user, according to Kevin Hartnett's book 'The Proof in the Code'. In 2017 Avigad's graduate student Mario Carneiro, working with Johannes Hölzl, started the mathematical library mathlib, which now holds nearly 300,000 theorems, over 100,000 definitions and 2.5 million lines of code from over 700 contributors.

The core claim is that autoformalization, meaning AI that reads a paper and outputs a formal proof in Lean or another proof assistant, has become a practical reality in 2026. For scale, the human-written formal proof of the Kepler conjecture took about 20 human work-years and about 500,000 lines of proof scripts. Hales lists milestones: in September 2025 Math Inc. produced a 'quasi-autoformalization' of the prime number theorem, where humans had to step in whenever the AI got stuck; in January 2026 J. Urban posted the preprint '130k lines of formal topology in two weeks' on large parts of Munkres's topology textbook; in March 2026, about a week after announcing the 8-dimensional case, Math Inc. announced an autoformalization of sphere packing in 24 dimensions, about 500K lines of source code that golfing (code pruning) later cut to about 200K; in May 2026 a group at Meta/Facebook Research autoformalized a large part of 26 mathematical textbooks in a project called ATLAS. He singles out the autoformalization of Fermat's Last Theorem, announced by Anthropic on September 4, which generated 13 million lines of Lean in 11 days, and the Navier-Stokes blowup-with-forcing announcement by OpenAI on September 8, which came with a Lean autoformalization of the theorem. Looking ahead he cites Urban's January statement that '(auto)formalization may become quite easy and ubiquitous in 2026', IEEE Spectrum's description of Jesse Han seeing the start of a revolution of extremely large-scale formalizations, and Jared Lichtman's launch of MAP, the Mathematics Autoformalization Project, on September 8, 2026, which aims to translate 'all known math into formal code'.

The second half asks whether Lean is reliable. Lean is based on the calculus of inductive constructions, a dialect of type theory. Hales gives a short history (Russell's paradox, Zermelo's set theory versus Russell's type theory) and notes that B. Werner's 1997 paper 'Sets in Types, Types in Sets' shows ZFC can be encoded into the calculus of inductive constructions and a dialect of it back into ZFC, augmented with a hierarchy of inaccessible cardinals. Lean is both a programming language and a mathematical language. Proof scripts are parsed, go through elaboration, and are then checked by the Lean kernel, which is several thousand lines of C++, carefully engineered but extremely complex. If mathlib contains an unconditional false proof, he writes, it is the fault of the kernel or runtime for failing to reject it.

His rules are two. Lean proofs should never be believed until checked by the kernel, and a proof should not be accepted until a human audit confirms statement fidelity: is the verified theorem what we think it is, and do the Lean definitions match the intended ones? He says that task is generally massively easier than checking the proof. For Navier-Stokes, a human should compare the Lean statement with Fefferman's statement of the Millennium Prize Problem and check that real numbers, partial derivatives and measure are defined correctly. The comparator tool in Lean helps with this and can also inspect for unauthorized axioms.

The last section covers the 'Summer of Soundness Bugs'. A soundness bug lets the kernel accept a proof of 'False', and so of any proposition, which Hales calls the most disastrous kind of bug in a proof assistant. He found one in HOL Light in 2003, whose kernel is just a few hundred lines; it was the first found there since 1996. Lean 4 was released in September 2023 after two soundness bugs were found and corrected; another, caused by overflow, was reported in May 2025. Several more were uncovered in July and August 2026, and the turmoil affected various proof assistants. One Lean bug led to an illicit disproof of the Collatz conjecture; Hales learned of it when it produced a short illicit proof of the Kepler conjecture in Lean. All the bugs were quickly repaired and mathlib has been verified by the repaired kernel; de Moura's postmortem analyzes them. Hales calls the detection a positive development: 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, a co-author of 'CakeML: a verified implementation of ML', found the Collatz bug, and Dan Selsam found several others. The available text ends partway through de Moura's report on Selsam's work.

Key facts

Thomas Hales argues autoformalization, AI turning a paper into a formal Lean proof, has become a practical reality in 2026, citing the Anthropic Fermat's Last Theorem project (13 million lines of Lean in 11 days, announced September 4).
For scale, the human formal proof of the Kepler conjecture took about 20 work-years and about 500,000 lines; Math Inc.'s 24-dimensional sphere packing autoformalization produced about 500K lines, pruned to about 200K.
mathlib now has nearly 300,000 theorems, over 100,000 definitions and 2.5 million lines of code from over 700 contributors, all checked by a Lean kernel of several thousand lines of C++.
Several Lean soundness bugs surfaced in July and August 2026, including one that allowed an illicit disproof of the Collatz conjecture; Hales says all were quickly repaired and mathlib was re-verified by the repaired kernel.
His rules: never believe a Lean proof until the kernel checks it, and do not accept it until a human audit confirms the theorem statement is the intended one.

Why it matters

Proof assistants have long been limited by human labor: the Kepler conjecture took about 20 work-years to formalize. Hales says AI has removed that limit, pointing to 13 million lines of Lean produced in 11 days for Fermat's Last Theorem and a Lean autoformalization accompanying OpenAI's Navier-Stokes announcement. When proofs arrive in such volume, the question shifts from 'can it be formalized' to 'can the checker be trusted', which is why the post spends its second half on the kernel, soundness bugs and statement fidelity. The post also notes that the same AI that writes proofs helped find the kernel bugs.

Who it affects

Working mathematicians who use or are considering Lean and mathlib are the intended audience. Mathlib contributors (over 700) and the Lean developers who maintain the kernel are directly affected by the bug findings. AI labs and companies producing autoformalizations (Math Inc., Anthropic, OpenAI, Meta/Facebook Research) and organizers of large efforts such as MAP also depend on the kernel being sound. Security researchers using AI against proof-assistant kernels are named as the ones who found this summer's bugs.

How to use it

The post offers a working checklist rather than a product. First, treat a Lean proof as unproven until the kernel has checked it. Second, have a human audit statement fidelity, comparing the Lean statement and definitions with the intended mathematical statement; Hales says this is generally massively easier than checking the proof. Third, use the comparator tool in Lean, which assists with that audit and can inspect for unauthorized axioms. Existing results in mathlib, such as the Cauchy-Schwarz inequality, can be cited rather than reproved.

How solid is it

This is a first-person essay by Thomas Hales, who describes his own experience with formalization, including finding a HOL Light soundness bug in 2003. The claims about Lean's reliability, the 'practical reality' of autoformalization and the positive reading of the bug discoveries are his judgments. The milestones and the Anthropic and OpenAI announcements are reported by him, not independently checked here. The available text breaks off mid-sentence in the 'Summer of Soundness Bugs' section, so the rest of that section is not covered. An editor's note says the post was converted from another file format using AI.

Risks and caveats

A soundness bug is the worst failure a proof assistant can have, since it lets 'False' and therefore any proposition be proved; the Collatz disproof shows it happened in Lean this summer. The Lean kernel is described as carefully engineered but extremely complex, and Hales says any defect in the underlying type theory is a serious kernel defect if implemented in code. Passing the kernel is not enough: a proof can verify a statement that is not the intended one. The text does not say that the Fermat's Last Theorem or Navier-Stokes formalizations have been human-audited for statement fidelity. Urban's January remark was a prediction ('may become quite easy and ubiquitous'), not a report of a finished change.

“Lean proofs should never be believed until they have been checked by the kernel.”

— Thomas Hales