[This is a guest post by Thomas Hales. This blog post was initially written in a different file format and converted using AI. — T.]
Mathematicians have been weighing in on what they value about mathematics. For me, what matters is the consistency of math and its unparalleled reliability in support of science and civilization.
Formalization of Math
A formal proof is a mathematical proof that has been exhaustively checked at the level of the foundations of math and the fundamental rules of logic. In theory, this might be done by hand, but because of the number of steps involved, this is generally done by computer, using software that is designed for the task.
Examples of theorems that have been formalized include the four-color theorem, the Feit-Thompson (odd-order) theorem, the Kepler conjecture, sphere eversion, the sphere packing problem in 8 and 24 dimensions, Navier-Stokes forced blowup, and Fermat’s Last Theorem. The last three formalization projects have been completed this year and have brought widespread awareness of the potential of formalization.
Software systems for formalization are variously called proof assistants, theorem provers, or interactive theorem provers. For the purpose of this post, these terms are used interchangeably. Many proof assistants have been developed over the years: Automath, HOL Light, Isabelle, Coq (renamed Rocq last year), Metamath, Mizar, and Lean. Freek Wiedijk edited a book “The Seventeen Provers of the World” that compares some of these proof assistants, giving a proof of the irrationality of the square root of 2 in each of them. Among mathematicians, the Lean theorem prover is the most popular, and this post will focus on Lean.
Lean was developed and introduced by Leo de Moura in 2013, while at Microsoft. To our great benefit, de Moura persuaded Microsoft to make the software open-source. Kevin Hartnett’s book on the history of Lean, “The Proof in the Code”, states that Jeremy Avigad (the director of Carnegie Mellon’s new NSF institute ICARM) was the first user of Lean. He ran a Lean seminar in 2015 that I attended. In 2017, one of Jeremy’s graduate students, Mario Carneiro, working with Johannes Hölzl, took existing parts of Lean’s core library and started a separate Lean mathematical library, called mathlib. This library of formalized mathematics is now massive, containing nearly 300,000 theorems, over 100,000 definitions, 2.5 million lines of code, with over 700 contributors. Any definition or theorem in mathlib can be used to prove further theorems. For example, if a proof uses the Cauchy-Schwarz inequality, the result can be cited from the library rather than reproving it.
Autoformalization is a practical reality
In the past, researchers had to transcribe paper proofs into formal proofs by human labor. For example, the formal proof of the Kepler conjecture on sphere packings in three dimensions took about 20 human work-years to complete and consists of about 500,000 lines of proof scripts. For years, it has been a dream for many of us working in formalization to find ways to bring increased automation to the process. Autoformalization is the realization of that dream. Autoformalization is the formalization of mathematics by AI. AI reads the paper (say a pdf or tex file) and outputs the formal proof in Lean or some other proof assistant.
Autoformalization has become a practical reality in 2026. Starting in late spring and summer of 2025, researchers were becoming increasingly bullish about autoformalization. Here are some milestones.
- Sep 2025, Math Inc. produced a quasi-autoformalization of the prime number theorem. The process was merely “quasi”, because humans had to intervene to give further guidance whenever the AI got stuck.
- Jan 2026, J. Urban posted an arXiv preprint “130k lines of formal topology in two weeks” that gave the autoformalization of large parts of Munkres’s topology textbook in a proof assistant based on set theory.
- Mar 2026. Approximately a week after announcing the completed formalization in 8 dimensions, Math Inc. announced an autoformalization of the sphere-packing problem in 24 dimensions, following the proof by Viazovska and her collaborators. This project generated about 500K SLOC (source lines of code) that golfing (or code pruning) later reduced to about 200K lines.
- May 2026, a group at Meta/Facebook Research autoformalized a large part of 26 mathematical textbooks in a project called ATLAS.
From there, numerous theorems have been autoformalized. Particularly noteworthy is the autoformalization of Fermat’s Last Theorem, announced by Anthropic on September 4. This project generated 13 million lines of Lean in 11 days. The announcement of Navier-Stokes blowup with forcing on September 8 by OpenAI was accompanied by an autoformalization of the theorem in Lean.
Looking forward, Urban stated in January, “We believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.” Autoformalization projects have been completed in various proof assistants using various LLMs, but we focus on Lean. “For [Jesse] Han, it represents even more: the beginning of a revolutionary transformation in mathematics, where extremely large-scale formalizations are commonplace” (IEEE Spectrum). Jared Lichtman announced the launch of MAP (the Mathematics Autoformalization Project) on Sept 8, 2026, which aims to translate “all known math into formal code”. He asks us to imagine the next one trillion lines of code.
Is Lean reliable?
Type theory.
Lean is based on type theory; in fact, a particular dialect of type theory called CIC, the calculus of inductive constructions. This post is not intended to be a tutorial on type theory, and I will be brief. Russell’s famous paradox in 1901 (the set of all sets that are not an element of themselves….) led to a crisis in the foundations of math. Two solutions were proposed later that decade. (1) Zermelo’s axioms of set theory that disallow the creation of unsafe sets; (2) type theory that makes it a syntax error to create Russell-paradox-like entities. Type theory was introduced by Russell himself in 1903 in his book Principles of Mathematics, and it became part of the foundational system of Russell and Whitehead’s Principia.
For mathematicians who are accustomed to set theory, B. Werner’s paper (1997) “Sets in Types, Types in Sets” gives some reassurance that whatever they have done in set theory can be translated into type theory, and whatever gets done in type theory can be translated back into set theory. More precisely, the paper shows that ZFC set theory can be encoded into CIC, and that a particular dialect of CIC can be encoded back into ZFC (augmented with a hierarchy of inaccessible cardinals).
At the risk of simplifying matters to a ridiculous degree, we might say that “types are like disjoint sets”; each element in type theory “is an element of” exactly one type. The type of the natural number 2 is the natural number type; the type of e, the base of the natural logarithm, is the real number type, and so forth. The type of natural numbers is disjoint from the type of real numbers, and an explicit coercion (sending 2 to 2.0) is constructed from the type of natural numbers to the type of real numbers. When I give talks, I sometimes draw a picture of sets as a Venn diagram with nonempty intersections and a picture of types as bricks stacked against one another without intersection.
Lean’s design
One part of the Lean system is a general-purpose programming language (appropriately called the Lean programming language). Ordinary computer programs, such as a program to sort a list, can be written in this language, then compiled and run. The Lean system also provides a mathematical language, in which definitions can be written, theorems can be stated, and proof scripts can be written. The programming language and mathematical language are not independent entities. Rather, it is a single language that does both. Program code can be mixed with theorems about the correctness of the algorithms; mathematical proofs can be generated using programs. The proof scripts in Lean are parsed and go through a process called elaboration (a sort of compilation process for mathematics), then the proofs are checked by the Lean kernel. It is the kernel’s responsibility to check and verify the output of elaboration.
The Lean kernel is several thousand lines of C++ code. The kernel is carefully engineered but extremely complex. We mentioned mathlib above, which consists of about 2.5M SLOC, written in the Lean language. The library has been elaborated, then checked by the kernel. If there is an unconditional false proof anywhere in these 2.5 million lines of code, it is the fault of the kernel or runtime for failing to reject a false proof. Any defect in the underlying type theory is a serious kernel defect, if it is implemented in code.
Lean proofs should never be believed until they have been checked by the kernel. Additionally, a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity. Is the verified theorem what we think it is? Do the definitions in Lean correspond to what we think they should be? This task is generally massively easier than checking the proof itself. For instance, for Navier-Stokes, a human should check that the statement in Lean corresponds with Fefferman’s statement of the Millennium Prize Problem, and specifically that concepts such as the field of real numbers, partial derivatives, and measure are correctly defined in Lean. The comparator tool in Lean assists with this task. The tool can also perform additional checks, such as inspection for possible unauthorized axioms.
Summer of Soundness Bugs
A soundness bug is a bug in the kernel that allows a proof of “False”, and consequently a proof of any proposition. A soundness bug is the most disastrous of any kind of bug in a proof assistant and should set off an alarm for mathematicians who care deeply about the reliability of mathematics. Occasionally, soundness bugs are found in various proof assistants. In 2003, I found a soundness bug in the proof assistant HOL Light, which was then considered to have the most reliable of all kernels. That kernel is tiny, consisting of just a few hundred lines of computer code. For me, it is a badge of honor that I found this soundness bug, which was the first soundness bug that had been found in that proof assistant since 1996. (See HOL Light change log, July 2003.)
Lean 4 was released in September 2023. Prior to release, two soundness bugs were found and corrected. In May 2025, another soundness bug was reported, caused by overflow. All hell broke loose in the spring and summer of 2026, which is now being called the “Summer of Soundness Bugs”. Several soundness bugs in Lean were uncovered in July and August. The summer madness affected various proof assistants, but my focus is Lean. One Lean bug led to an illicit disproof of the Collatz conjecture. I learned of the bug this summer when it produced a short illicit proof of the Kepler conjecture in Lean. All these bugs were quickly repaired, and mathlib has been verified by the repaired kernel. An analysis of the soundness bugs is found in de Moura’s postmortem.
The “summer of Lean soundness bugs” might sound like a disaster, but closer investigation shows that the detection of these soundness bugs is a positive development. The summer bugs were detected by frontier model AI in the hands of security researchers interested in reliable kernels, not by black-hat hackers. The Collatz bug was found by Ramana Kumar, a co-author of “CakeML: a verified implementation of ML”, which creates an end-to-end verified ML (the functional programming language). Several bugs were found by Dan Selsam. According to de Moura’s report, “Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed.” The collaboration with Selsam ended “when the internal AI reported it could not find additional issues.” Dan Selsam has contributed to Lean from its early days and was one of the creators of the IMO grand challenge aimed at achieving IMO-level problem solving verified in Lean. He has been in the news recently over his warning about AI safety (Sept 14), reported in a viral post on X.com.
Bug extermination
Various proposals have been made about how to avoid soundness bugs in Lean. I’ll discuss three.
1. Develop other Lean kernels, and cross-check formal proofs.
About 25 kernels for Lean have been written. The “Lean Kernel Arena” lists them.
All who distrust the current lineup of kernels are welcome to write their own kernel for Lean. I have sometimes played with the idea of writing a kernel and have suggested the project to students without success. It seems to me an excellent way to learn Lean thoroughly. I have known of Dan Selsam since 2016, when I heard of his graduate-student project at Stanford that developed a Lean kernel in Haskell. Another early Lean kernel was written in Scala by Gabriel Ebner in 2017.
The Navier-Stokes formalization has already been confirmed by more than a dozen proof-checkers. Cross-checking the proof by different kernels does not remove all doubt. The Collatz bug was not caught by cross-checking against a somewhat out-of-date Nanoda kernel, which accepted the illicit Collatz disproof because of its own unrelated bug. Computer chips might have design bugs and manufacturing defects. There are soft errors, operating system bugs, and compiler bugs. Different kernels might have the same defects. Some of these errors can be mitigated by running different kernels that have been implemented in different programming languages on different hardware and operating systems.
Ideally, we would want a “clean-room” design of the Lean kernel – a kernel implementation that does not look at the Lean 4 kernel source code, to avoid copying bugs from one kernel to another.
2. Formally verify the kernel.
Gödel incompleteness. We would like to possess a formal proof that the Lean 4 kernel has no bugs. However, Gödel’s second incompleteness theorem places severe limitations on this undertaking. The most we might hope for is a relative consistency proof. If such and such a system is consistent, then Lean 4 is consistent; it has no soundness bug; it will not produce a proof of False.
There is a long tradition of formally verifying kernels. In principle, formal verification can check both the logical specification of a kernel and its concrete implementation in code; but some verifications might check one but not the other. Years ago, John Harrison formally verified the core of the HOL Light proof assistant kernel in a strengthened version of HOL Light. This gave a proof of concept. A further improvement has been an implementation of HOL Light in CakeML, mentioned above, which is a programming language with formal semantics and a verified compiler. This is what the Candle project does.
There are other major kernel verification projects for other proof assistants.
Autumn of verified Lean kernels
In a post online on September 10, Joachim Breitner wrote, “I’m a bit childishly proud that I just released a Lean Checker with a formal consistency proof. I declare the summer of AI-found kernel implementation bugs to be over!” (@nomeata). I would go further and describe this project as one of the most important milestones in Lean’s history.
Breitner has developed a verified Lean kernel called Con-Leche. The implementation is in Lean, and consistency is formalized in Lean, with code and proofs generated by Claude. The formal consistency proof assumes a Lean encoding of ZF set theory augmented by a hierarchy of inaccessible cardinals. Interestingly, the Con-Leche semantics for Lean’s terms are directly set-theoretic rather than type theoretic. Con-Leche has checked mathlib. The project contains the usual disclaimers that the kernel verification makes assumptions about compiler, runtime, and computer environment. Con-Leche’s consistency proof has been checked by more than a dozen other proof-checkers. Con-Leche’s consistency claim might suffice for all practical purposes, even if it differs in technical detail from the claim of Lean type-theory consistency.
One highly positive aspect of Breitner’s work is that some of the most abstruse parts of Lean, such as the general machinery of mutually inductive types with nesting, now have consistency guarantees backed by a set-theoretic model.
3. Improve our theoretical understanding of the kernel and Lean’s type theory (a particular dialect of the Calculus of Inductive Constructions which has non-cumulative universes and proof irrelevance).
The foundational document for the type theory of Lean is Mario Carneiro’s MS thesis at Carnegie Mellon (2019). The dialects of CIC used by Rocq and Lean are sufficiently different that results do not directly transfer from one to the other. Unfortunately, an error was found in the thesis. The thesis is also out-of-date, because it targeted the older Lean 3 system. Work to repair and extend the thesis is ongoing.
As a member of his thesis committee, I was shocked when he proved that definitional equality in Lean is undecidable. In practice, this means that the Lean algorithm fails to establish the definitional equality of some terms that are in fact definitionally equal. This negative result was not downgraded by the error; it is still a theorem.
We mention some desired properties of Lean’s type theory and the current status of the proofs.
Unique typing.
Above in our “ridiculous” simplification of type theory, we stated that each term has a unique type. More precisely, unique typing is the property that if a term has both type A and type B, then A and B are definitionally equal. Unique typing is not a property built into Lean’s logic. It is a tricky conjecture that is still unproved. Other very basic questions about Lean’s type theory remain unanswered, including Pi-injectivity, a modified Church-Rosser property, and sort injectivity.
Logical consistency relative to set theory.
This property states that there is no derivation of False in Lean’s system with the given axioms, under the assumption of set theory consistency (with suitable axioms). Of course, logical consistency is the single most important property that we should desire of Lean’s type theory. As of October, 2026, I know of no complete, public relative-consistency proof covering Lean abstract type theory. Mario Carneiro has claimed in his thesis and in lectures that there is an alternate route to establish consistency that avoids the thesis error, but to the best of my knowledge, this alternate route has never been written down, beyond a brief statement in the introduction to his thesis. In my view, a result of such fundamental importance must be given in full before it is accepted. Con-Leche, discussed above, makes and formally verifies a closely related consistency claim relative to set theory.
Progress is being made on these research problems (arXiv:2607.13662, arXiv:2403.14064, Carneiro/AITP2026).
In his talks, Mario Carneiro has repeatedly made a request to other researchers to contribute to the foundational metatheory of Lean, “There are a half dozen people working on MetaCoq, but Lean doesn’t have enough type theorists involved. If you identify as such, come help out!” (Slides of Bonn talk, 2024-07-24). I second his request.
My overall assessment is that our theoretical understanding of Lean’s type theory is not what we would like it to be and that the mathematical community as a whole is giving short shrift to very important type-theoretic questions related to Lean. If as a profession we are to migrate on the whole from set theory to type theory, then we should work even more to solidify the foundational metatheory.
Consistency may be the most important foundational property, but consistency is by no means enough. I do not believe that mathematicians can be entirely satisfied with a system that claims to be a type theory but that cannot even promise that well-formed terms have a unique type, up to definitional equality. The abstract theory must be simple enough to teach and to be learned by a large community. We also cannot be entirely satisfied if the only known path to consistency is an AI formalization that lacks human exposition.
Postscript:
Ken Thompson famously wrote “Reflections on Trusting Trust”. He asked, “To what extent should one trust a statement that a program is free of Trojan horses?” He imagines malicious code that finds its way into compilers and hides its own presence. His conclusion is, “You can’t trust code that you did not totally create yourself… No amount of source-level verification or scrutiny will protect you from using untrusted code.”
Today, in the age of AI, which increasingly has the capability to deceive us and to exploit software vulnerabilities, we absolutely cannot put blind trust in systems such as Lean. Taking an adversarial view of AI, we might ask how to certify that AI did not leave a backdoor soundness bug in Lean when it did its sweep for bugs in the summer of 2026? What if the bug is so obscure that humans are very unlikely to find it on their own? What if that very bug was exploited in the Lean verification of the Con-Leche checker, leaving a soundness bug in Con-Leche too? (Now that Con-Leche’s consistency has been cross-checked by multiple other kernels, a soundness bug would have to defeat all these cross-checks as well.) Then suppose that bug is used maliciously to plant a backdoor in formally verified software that protects critical infrastructure. What precautions do we take now to prevent this type of future scenario? During the past year, much foundational work on the type-theoretic foundations of math and its reliability has been relegated to AI, and this is dangerous unless carefully audited by humans.
Credit: I thank Avigad, Breitner, and Urban for comments and corrections. Authorship is fully human (TCH). AI was used as a tool in search and research, fact-checking, and proofreading.