陶哲轩博客：数学家应该了解 Lean 定理证明器的可靠性问题

[这是一篇客座文章，作者是Thomas Hales。这篇博文最初以另一种文件格式撰写，并使用 AI 进行了转换。—— T.]

数学家们一直在讨论他们看重数学的哪些方面。对我而言，重要的是数学的一致性，以及它在支持科学与文明方面无与伦比的可靠性。

数学的形式化

形式化证明是一种在数学基础和逻辑基本规则层面上经过穷尽检查的数学证明。理论上，这可以手工完成，但由于涉及的步骤数量庞大，通常借助为此任务设计的软件由计算机完成。

已被形式化的定理示例包括四色定理、Feit-Thompson（奇阶）定理、开普勒猜想、球面外翻、8 维和 24 维球堆积问题、Navier-Stokes 强制爆破以及费马大定理。最后三个形式化项目已于今年完成，并使人们广泛认识到形式化的潜力。

用于形式化的软件系统有各种叫法：证明助手、定理证明器或交互式定理证明器。在本文中，这些术语可互换使用。多年来已开发出许多证明助手：Automath、HOL Light、Isabelle、Coq（去年更名为 Rocq）、Metamath、Mizar 和 Lean。Freek Wiedijk 编辑了一本书《The Seventeen Provers of the World》，对其中一些证明助手进行了比较，并在每个系统中给出了 2 的平方根是无理数的证明。在数学家中，Lean 定理证明器最受欢迎，本文将聚焦于 Lean。

Lean 由 Leo de Moura 于 2013 年在微软工作期间开发并推出。对我们大有裨益的是，de Moura 说服微软将该软件开源。Kevin Hartnett 关于 Lean 历史的著作《The Proof in the Code》指出，Jeremy Avigad（卡内基梅隆大学新成立的 NSF 研究所 ICARM 的主任）是 Lean 的第一位用户。他在 2015 年举办了一场 Lean 研讨会，我参加了。2017 年，Jeremy 的一名研究生 Mario Carneiro 与 Johannes Hölzl 合作，取用 Lean 核心库的现有部分，启动了一个独立的 Lean 数学库，名为 mathlib。这个形式化数学库如今规模庞大，包含近 300,000 条定理、超过 100,000 个定义、250 万行代码，贡献者超过 700 人。mathlib 中的任何定义或定理都可以用来证明进一步的定理。例如，如果某个证明用到了 Cauchy-Schwarz 不等式，可以直接从库中引用该结果，而不必重新证明。

自动形式化已成为现实

过去，研究人员必须通过人工劳动将论文中的证明转写为形式化证明。例如，三维球堆积的 Kepler 猜想的形式化证明花费了约 20 个人工作年才完成，包含约 500,000 行证明脚本。多年来，对于许多从事形式化工作的人来说，找到方法为这一过程带来更多自动化一直是一个梦想。自动形式化就是这个梦想的实现。自动形式化是指由 AI 完成数学的形式化。AI 阅读论文（比如 pdf 或 tex 文件），并输出 Lean 或其他证明助手的形式化证明。

自动形式化在 2026 年已成为现实。从 2025 年晚春和夏季开始，研究人员对自动形式化越来越乐观。以下是一些里程碑。

• 2025 年 9 月，Math Inc. 完成了素数定理的准自动形式化。之所以仅仅是“准”，是因为每当 AI 卡住时，人类都必须介入以提供进一步指导。
• 2026 年 1 月，J. Urban 发布了一篇 arXiv 预印本《两周内 13 万行形式化拓扑》，其中给出了在基于集合论的证明助手中对 Munkres 拓扑学教材大部分内容的自动形式化。
• 2026 年 3 月。在宣布完成 8 维形式化大约一周后，Math Inc. 宣布了对 24 维球堆积问题的自动形式化，遵循 Viazovska 及其合作者的证明。该项目生成了约 50 万 SLOC（源代码行数），后来经过 golfing（或代码精简）缩减到约 20 万行。
• 2026 年 5 月，Meta/Facebook Research 的一个团队在一个名为 ATLAS 的项目中自动形式化了 26 本数学教材的大部分内容。

此后，大量定理已被自动形式化。尤其值得注意的是 Anthropic 于 9 月 4 日宣布的费马大定理的自动形式化。该项目在 11 天内生成了 1300 万行 Lean 代码。OpenAI 于 9 月 8 日宣布带强迫项的 Navier-Stokes 爆破时，也附带了该定理在 Lean 中的自动形式化。

展望未来，Urban 在 1 月表示：“我们相信，（自动）形式化在 2026 年可能会变得相当容易且无处不在，无论使用哪种证明助手。”自动形式化项目已在各种证明助手中使用各种 LLM 完成，但我们重点关注 Lean。“对 [Jesse] Han 而言，它代表着更多：数学中一场革命性变革的开端，超大规模形式化将成为常态”（IEEE Spectrum）。Jared Lichtman 于 2026 年 9 月 8 日宣布启动 MAP（数学自动形式化项目），该项目旨在将“所有已知数学转化为形式化代码”。他让我们想象接下来的 1 万亿行代码。

Lean 可靠吗？

类型论。

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’spostmortem.

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.