数学家应该了解 Lean 定理证明器的哪些事：可靠性与 AI

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

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

数学的形式化

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

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

用于形式化的软件系统有各种名称，如证明助手、定理证明器或交互式定理证明器。在本文中，这些术语可互换使用。多年来已开发出许多证明助手：Automath、HOL Light、Isabelle、Coq（去年更名为Rocq）、Metamath、Mizar和Lean。Freek Wiedijk编辑了一本书《世界十七个证明器》，比较了其中一些证明助手，并在每个系统中给出了√2无理性的证明。在数学家中，Lean定理证明器最受欢迎，本文将聚焦于Lean。

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

自动形式化已成为现实

过去，研究人员必须通过人力将论文证明转录为形式化证明。例如，三维球堆积的开普勒猜想的形式化证明花费了约20个人工年才完成，包含约50万行证明脚本。多年来，我们许多从事形式化工作的人一直梦想着找到方法为这一过程带来更多自动化。自动形式化就是这一梦想的实现。自动形式化是由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（数学自动形式化项目），旨在将“所有已知数学转化为形式化代码”。他让我们想象接下来的万亿行代码。

Lean 可靠吗？

类型论。

Lean 基于类型论；事实上，是一种被称为 CIC（归纳构造演算）的特定类型论方言。本文并非类型论教程，我将简要说明。罗素在 1901 年提出的著名悖论（所有不属于自身的集合所构成的集合……）导致了数学基础的危机。那个十年后期提出了两种解决方案。(1) Zermelo 的集合论公理，禁止创建不安全的集合；(2) 类型论，使创建类似罗素悖论的实体成为语法错误。类型论由罗素本人于 1903 年在其著作《数学的原理》中引入，并成为罗素和怀特海《数学原理》基础系统的一部分。

对于习惯集合论的数学家来说，B. Werner 的论文（1997 年）“Sets in Types, Types in Sets”提供了一些保证：他们在集合论中所做的一切都可以翻译成类型论，而在类型论中完成的一切都可以翻译回集合论。更准确地说，该论文表明 ZFC 集合论可以编码到 CIC 中，而 CIC 的一种特定方言可以编码回 ZFC（并加入不可达基数层级）。

冒着把问题过度简单化的风险，我们可以说“类型就像不相交的集合”；类型论中的每个元素都“属于”恰好一个类型。自然数 2 的类型是自然数类型；自然对数底 e 的类型是实数类型，依此类推。自然数类型与实数类型不相交，并且从自然数类型到实数类型构造了一个显式的强制转换（把 2 变为 2.0）。在演讲时，我有时会把集合画成带有非空交集的维恩图，而把类型画成彼此紧靠、互不相交的砖块。

Lean 的设计

Lean 系统的一部分是一种通用编程语言（恰如其分地称为 Lean 编程语言）。普通的计算机程序，例如对列表进行排序的程序，可以用这种语言编写，然后编译并运行。Lean 系统还提供了一种数学语言，可以用它编写定义、陈述定理并编写证明脚本。编程语言和数学语言并不是彼此独立的实体。相反，它是一种兼具两者功能的单一语言。程序代码可以与关于算法正确性的定理混合在一起；数学证明可以用程序生成。Lean 中的证明脚本会被解析，并经历一个称为 elaboration 的过程（一种针对数学的编译过程），然后证明由 Lean 内核检查。检查和验证 elaboration 的输出是内核的职责。

Lean 内核是数千行 C++ 代码。内核经过精心设计，但极其复杂。我们上面提到了 mathlib，它由约 250 万行源代码组成，用 Lean 语言编写。该库已经过 elaboration，然后由内核检查。如果这 250 万行代码中任何地方存在无条件为假的证明，那就是内核或运行时未能拒绝假证明的过错。底层类型论中的任何缺陷，如果它在代码中实现，就是严重的内核缺陷。

在 Lean 中的证明被内核检查之前，绝不应相信它们。此外，在 Lean 中的证明被接受之前，还应进行人工审计以确保陈述的忠实性。被验证的定理是否是我们认为的那个定理？Lean 中的定义是否对应于我们认为它们应该对应的内容？这项任务通常比检查证明本身容易得多。例如，对于 Navier-Stokes，人工应检查 Lean 中的陈述是否与 Fefferman 对千禧年大奖难题的陈述相对应，特别是实数域、偏导数和测度等概念在 Lean 中是否被正确定义。Lean 中的 comparator 工具可协助完成这项任务。该工具还可以执行额外的检查，例如检查是否存在可能的未经授权的公理。

健全性漏洞之夏

可靠性 bug 是内核中的一种 bug，它允许证明“False”，从而允许证明任何命题。可靠性 bug 是证明助手中最灾难性的 bug，应当为那些深切关心数学可靠性的数学家敲响警钟。偶尔，各种证明助手中会发现可靠性 bug。2003 年，我在证明助手 HOL Light 中发现了一个可靠性 bug，当时它被认为拥有所有内核中最可靠的内核。那个内核很小，仅由几百行计算机代码组成。对我来说，发现这个可靠性 bug 是一种荣誉，这是自 1996 年以来在该证明助手中发现的第一个可靠性 bug。（参见 HOL Light 变更日志，2003 年 7 月。）

Lean 4 于 2023 年 9 月发布。发布之前，发现并修正了两个可靠性 bug。2025 年 5 月，又报告了一个由溢出引起的可靠性 bug。2026 年春夏，一切都乱了套，如今被称为“可靠性 bug 之夏”。7 月和 8 月，Lean 中发现了若干可靠性 bug。这场夏季的疯狂影响了各种证明助手，但我关注的是 Lean。其中一个 Lean bug 导致了对 Collatz 猜想的非法反证。今年夏天，当它在 Lean 中生成一个简短的 Kepler 猜想非法证明时，我得知了这个 bug。所有这些 bug 都很快被修复，mathlib 已由修复后的内核验证。对可靠性 bug 的分析见 de Moura 的事后分析。

“Lean 可靠性 bug 之夏”听起来像是一场灾难，但更仔细的调查表明，这些可靠性 bug 的发现是一个积极的进展。夏季的这些 bug 是由前沿模型 AI 在关注可靠内核的安全研究人员手中检测到的，而不是由黑帽黑客发现的。Collatz bug 是由 Ramana Kumar 发现的，他是“CakeML：ML 的经过验证的实现”的合著者之一，该工作创建了一个端到端经过验证的 ML（函数式编程语言）。若干 bug 是由 Dan Selsam 发现的。根据 de Moura 的报告，“OpenAI 的 Daniel Selsam 用专门从事网络安全的 AI 协助 Lean FRO，并发现了 Lean 内核中的其他编程错误。所有这些都已修复。”与 Selsam 的合作在“内部 AI 报告无法发现更多问题”时结束。Dan Selsam 从早期就为 Lean 做出了贡献，并且是 IMO 大挑战的创建者之一，该挑战旨在实现 IMO 级别的、在 Lean 中经过验证的问题求解。他最近因对 AI 安全的警告（9 月 14 日）而登上新闻，X.com 上的一篇帖子对此进行了病毒式传播。

消灭 bug

关于如何避免 Lean 中的可靠性 bug，已经提出了各种建议。我将讨论三种。

1. 开发其他 Lean 内核，并交叉检查形式化证明。

大约 25 个 Lean 内核已被编写出来。“Lean Kernel Arena”列出了它们。

欢迎所有不信任当前内核阵容的人为 Lean 编写自己的内核。我有时也玩过编写内核的想法，并曾向学生建议过这个项目，但没有成功。在我看来，这是彻底学习 Lean 的绝佳方式。我自 2016 年就知道 Dan Selsam，当时我听说了他在斯坦福大学的研究生项目，该项目用 Haskell 开发了一个 Lean 内核。另一个早期的 Lean 内核是 Gabriel Ebner 在 2017 年用 Scala 编写的。

Navier-Stokes 形式化已被十多个证明检查器确认。用不同内核交叉检查该证明并不能消除所有疑虑。Collatz 漏洞并未被交叉检查发现，因为对照的是一个有些过时的 Nanoda 内核，它由于自身一个无关的漏洞而接受了那个非法的 Collatz 反证。计算机芯片可能有设计缺陷和制造缺陷。还有软错误、操作系统漏洞和编译器漏洞。不同内核可能有相同的缺陷。其中一些错误可以通过在不同硬件和操作系统上运行用不同编程语言实现的不同内核来缓解。

理想情况下，我们希望 Lean 内核采用“洁净室”设计——一种不查看 Lean 4 内核源代码的内核实现，以避免将一个内核的漏洞复制到另一个内核。

2. 形式化验证内核。

哥德尔不完备性。我们希望拥有一个形式化证明，证明 Lean 4 内核没有漏洞。然而，哥德尔第二不完备定理对这一努力施加了严重限制。我们最多只能期望一个相对一致性证明。如果某某系统是一致的，那么 Lean 4 就是一致的；它没有可靠性漏洞；它不会产生 False 的证明。

形式化验证内核有着悠久的传统。原则上，形式化验证可以同时检查内核的逻辑规范和其具体代码实现；但有些验证可能只检查其中之一而不检查另一个。多年前，John Harrison 在 HOL Light 的一个强化版本中形式化验证了 HOL Light 证明助手内核的核心。这提供了一个概念验证。进一步的改进是上文提到的在 CakeML 中实现 HOL Light，CakeML 是一种具有形式化语义和经过验证的编译器的编程语言。这就是 Candle 项目所做的。

还有其他针对其他证明助手的主要内核验证项目。

经过验证的 Lean 内核之秋

在 9 月 10 日的一篇在线帖子中，Joachim Breitner 写道：“我有点孩子气地感到自豪，因为我刚刚发布了一个带有形式化一致性证明的 Lean 检查器。我宣布 AI 发现内核实现漏洞的夏天结束了！”（@nomeata）。我要更进一步，将这个项目描述为 Lean 历史上最重要的里程碑之一。

Breitner 开发了一个经过验证的 Lean 内核，名为 Con-Leche。其实现用 Lean 编写，一致性也在 Lean 中形式化，代码和证明由 Claude 生成。形式化一致性证明假设了一个 ZF 集合论的 Lean 编码，并附加了不可达基数的层级。有趣的是，Con-Leche 对 Lean 项的语义是直接集合论的，而非类型论的。Con-Leche 已检查了 mathlib。该项目包含通常的免责声明，即内核验证对编译器、运行时和计算机环境做出了假设。Con-Leche 的一致性证明已被十多个其他证明检查器检查过。Con-Leche 的一致性声明对于所有实际目的可能已经足够，即使它在技术细节上与 Lean 类型论一致性的声明有所不同。

Breitner 工作的一个非常积极的方面是，Lean 中一些最晦涩的部分，例如带嵌套的互归纳类型的一般机制，现在有了由集合论模型支持的一致性保证。

3. 增进我们对内核和 Lean 类型论（归纳构造演算的一种特定方言，具有非累积宇宙和证明无关性）的理论理解。

Lean 类型论的基础性文献是 Mario Carneiro 在卡内基梅隆大学的硕士论文（2019 年）。Rocq 和 Lean 所使用的 CIC 方言差异足够大，因此结果无法直接从一个系统迁移到另一个系统。遗憾的是，该论文中发现了一个错误。该论文也已过时，因为它针对的是较旧的 Lean 3 系统。修复和扩展该论文的工作正在进行中。

作为他论文委员会的成员，当他证明 Lean 中的定义相等性是不可判定的时候，我感到震惊。在实践中，这意味着 Lean 算法无法为某些实际上定义相等的项建立定义相等性。这一否定性结果并未因该错误而被降级；它仍然是一个定理。

我们提及 Lean 类型论的一些期望性质以及这些证明的当前状态。

唯一类型。

在上文我们对类型论的“荒谬”简化中，我们指出每个项都有唯一的类型。更准确地说，唯一类型是指：如果一个项同时具有类型 A 和类型 B，那么 A 和 B 是定义相等的。唯一类型并不是 Lean 逻辑中内置的性质。它是一个尚未被证明的棘手猜想。关于 Lean 类型论的其他非常基本的问题仍未得到解答，包括 Pi 单射性、一种修改后的 Church-Rosser 性质以及宇宙单射性。

相对于集合论的逻辑一致性。

该性质指出，在集合论一致性（加上适当的公理）的假设下，Lean 系统中给定公理不会推导出 False。当然，逻辑一致性是我们应当期望 Lean 类型论具备的最重要的单一性质。截至 2026 年 10 月，据我所知，还没有一个完整的、公开的、覆盖 Lean 抽象类型论的相对一致性证明。Mario Carneiro 在他的论文和讲座中声称，存在一条避开论文错误的替代路径来建立一致性，但据我所知，除了他论文引言中的简短陈述之外，这条替代路径从未被写下来。在我看来，如此重要的结果必须完整给出后才能被接受。上文讨论的 Con-Leche 提出并形式化验证了一个与集合论密切相关的相对一致性断言。

这些研究问题正在取得进展（arXiv:2607.13662、arXiv:2403.14064、Carneiro/AITP2026）。

在他的演讲中，Mario Carneiro 多次请求其他研究人员为 Lean 的基础元理论做出贡献，“有半打人在研究 MetaCoq，但 Lean 没有足够的类型论学者参与。如果你自认是其中一员，来帮忙吧！”（波恩演讲幻灯片，2024-07-24）。我附议他的请求。

我的总体评估是，我们对 Lean 类型论的理论理解尚未达到我们期望的水平，而且整个数学界对与 Lean 相关的非常重要的类型论问题重视不足。如果我们作为一个专业整体要从集合论迁移到类型论，那么我们就更应该努力夯实基础元理论。

一致性也许是最重要的基础性质，但一致性远远不够。我不相信数学家们会完全满意一个自称是类型论、却甚至不能保证良构项在定义相等意义下具有唯一类型的系统。抽象理论必须足够简单，以便能够被教授并被广大群体学习。如果已知的唯一一致性路径是缺乏人类阐述的 AI 形式化，我们也不能完全满意。

后记：

Ken Thompson 写下了著名的《关于信任的反思》。他问道：“在多大程度上，人们应当相信一个程序没有特洛伊木马的陈述？”他设想恶意代码进入编译器并隐藏自身的存在。他的结论是：“你不能信任并非完全由你自己创建的代码……任何程度的源码级验证或审查都无法保护你免于使用不可信的代码。”

如今，在 AI 时代，AI 越来越有能力欺骗我们并利用软件漏洞，我们绝对不能盲目信任 Lean 这样的系统。以对抗性的视角看待 AI，我们可能会问：当 AI 在 2026 年夏天对 Lean 进行漏洞扫描时，如何证明 AI 没有在 Lean 中留下后门可靠性漏洞？如果这个漏洞极其隐蔽，人类极不可能自行发现呢？如果正是这个漏洞在 Con-Leche 检查器的 Lean 验证中被利用，从而也在 Con-Leche 中留下了一个可靠性漏洞呢？（既然 Con-Leche 的一致性已被多个其他内核交叉检查，那么一个可靠性漏洞还必须同时击败所有这些交叉检查。）然后假设这个漏洞被恶意用于在保护关键基础设施的形式化验证软件中植入后门。我们现在应采取哪些预防措施来防止这种未来场景？在过去一年中，许多关于数学的类型论基础及其可靠性的基础工作被交给了 AI，除非由人类仔细审计，否则这是危险的。

致谢：我感谢 Avigad、Breitner 和 Urban 的评论与更正。作者身份完全由人类完成（TCH）。AI 被用作搜索与研究、事实核查和校对中的工具。