数学家应该了解的 Lean 定理证明器：可靠性与人工智能

# 数学家应该了解的 Lean 定理证明器：可靠性与 AI 相关问题 来源：https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/ *\本文是 [Thomas Hales](https://www.mathematics.pitt.edu/people/thomas-hales) 的客座文章。本博客文章最初以其他文件格式撰写，后经 AI 转换。——T.\* 数学家们一直在探讨数学的价值所在。对我而言，数学的意义在于其一致性，以及它对科学和文明无与伦比的支撑可靠性。 **数学的形式化** 形式化证明是指在数学基础和基本逻辑规则层面经过穷尽式检查的数学证明。理论上这可以手动完成，但由于涉及的步骤数量庞大，通常由计算机执行，使用为此任务专门设计的软件。 已被形式化的定理示例包括四色定理、Feit-Thompson 定理（奇数阶定理）、开普勒猜想、球面翻转（sphere eversion）、8 维和 24 维球体堆积问题、Navier-Stokes 强迫爆破解，以及费马大定理。最后三个形式化项目于今年完成，广泛引起了人们对形式化潜力的关注。 用于形式化的软件系统分别被称为证明辅助器（proof assistant）、定理证明器（theorem prover）或交互式定理证明器（interactive theorem prover）。在本文中，这些术语交替使用。多年来已开发出许多证明辅助器：Automath、HOL Light、Isabelle、Coq（去年更名为 Rocq）、Metamath、Mizar 和 Lean。Freek Wiedijk 编辑了一本书《The Seventeen Provers of the World》，在其中比较了部分证明辅助器，并分别给出了 $\sqrt{2}$ 无理性的证明。在数学家中，Lean 定理证明器最为流行，本文将聚焦于 Lean。 Lean 由 Leo de Moura 于 2013 年在 Microsoft 任职时开发并推出。让我们深感幸运的是，de Moura 说服了 Microsoft 将该软件开源。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 不等式，可以从库中直接引用结果，而无需重新证明。 **自动形式化已成为现实** 过去，研究者必须依靠人力将纸面证明转录为形式化证明。例如，关于三维球体堆积的开普勒猜想的形式化证明耗时约 20 个人年，包含约 500,000 行证明脚本。多年来，我们许多从事形式化工作的人都梦想着能为这一过程引入更多自动化手段。自动形式化（autoformalization）正是这一梦想的实现。自动形式化即由 AI 完成数学的形式化。AI 阅读论文（如 PDF 或 TeX 文件），然后输出 Lean 或其他证明辅助器中的形式化证明。 自动形式化在 2026 年已成为现实。自 2025 年晚春和夏季起，研究者们对自动形式化日益乐观。以下是部分里程碑： - 2025 年 9 月，Math Inc. 对素数定理进行了准自动形式化（quasi-autoformalization）。之所以称为"准"，是因为每当 AI 遇到困难时，仍需要人工介入提供进一步指导。 - 2026 年 1 月，J. Urban 在 arXiv 发布预印本《130k lines of formal topology in two weeks》，在基于集合论的证明辅助器中完成了 Munkres 拓扑学教材大部分内容的自动形式化。 - 2026 年 3 月。在宣布完成 8 维形式化约一周后，Math Inc. 宣布了 24 维球体堆积问题的自动形式化，基于 Viazovska 及其合作者的证明。该项目生成了约 50 万行源代码（SLOC），随后通过代码精简（golfing/code pruning）缩减至约 20 万行。 - 2026 年 5 月，Meta/Facebook Research 的一个团队在名为 ATLAS 的项目中自动形式化了 26 本数学教材的大部分内容。 此后，大量定理被自动形式化。其中尤为引人注目的是 Anthropic 于 9 月 4 日宣布的费马大定理自动形式化项目。该项目在 11 天内生成了 1300 万行 Lean 代码。OpenAI 于 9 月 8 日宣布的 Navier-Stokes 强迫爆破解成果，也伴随着该定理在 Lean 中的自动形式化。 展望未来，Urban 在一月表示："我们相信，自动形式化可能在 2026 年变得相当容易和普遍，无论使用哪种证明辅助器。"自动形式化项目已在各种证明辅助器中使用各种 LLM 完成，但本文聚焦于 Lean。"对于 [Jesse] Han 来说，这更意味着：数学革命性变革的开端，超大规模形式化将成为常态"（[IEEE Spectrum](https://spectrum.ieee.org/ai-proof-verification)）。Jared Lichtman 于 2026 年 9 月 8 日宣布启动 MAP（Mathematics Autoformalization Project，数学自动形式化项目），旨在将"所有已知数学翻译为形式化代码"。他邀请我们想象接下来的一万亿行代码。 **Lean 可靠吗？** **类型论。** Lean 基于类型论；确切地说，是一种名为 CIC（calculus of inductive constructions，归纳构造演算）的类型论特定分支。本文不是类型论教程，我将简要说明。Russell 于 1901 年提出的著名悖论（所有不包含自身作为元素的集合构成的集合……）引发了数学基础的危机。那十年间提出了两种解决方案。（1）Zermelo 的集合论公理，禁止构造不安全的集合；（2）类型论，使得构造类似 Russell 悖论的对象成为语法错误。类型论由 Russell 本人于 1903 年在其著作《Principles of Mathematics》中提出，并成为 Russell 和 Whitehead 的《Principia》基础体系的一部分。 对于习惯集合论的数学家来说，B. Werner 的论文《Sets in Types, Types in Sets》（1997）提供了一定的保证：他们在集合论中所做的任何工作都可以翻译到类型论中，而类型论中的任何工作也都可以翻译回集合论。更准确地说，该论文表明 ZFC 集合论可以编码到 CIC 中，而 CIC 的一种特定分支可以编码回 ZFC（扩充以不可达基数层级）。 冒着将问题过度简化的风险，我们可以说"类型就像互不相交的集合"：类型论中的每个元素恰好"属于"一个类型。自然数 2 的类型是自然数类型；自然对数底数 e 的类型是实数类型，以此类推。自然数类型与实数类型互不相交，因此需要构造一个显式强制转换（coercion）（将 2 映射为 2.0）从自然数类型转换到实数类型。我在演讲时有时会画两张图：将集合画成有非空交集的 Venn 图，将类型画成彼此堆叠而不相交的砖块。 **Lean 的设计** Lean 系统的一部分是通用编程语言（恰如其分地称为 Lean 编程语言）。普通计算机程序（如列表排序程序）可以用该语言编写，然后编译运行。Lean 系统还提供了一种数学语言，在其中可以编写定义、陈述定理、编写证明脚本。编程语言和数学语言并非独立的实体。相反，它是同时承担两种功能的单一语言。程序代码可以与关于算法正确性的定理混写；数学证明也可以通过程序生成。Lean 中的证明脚本经过解析后，会经历一个称为 elaboration（一种数学的编译过程）的处理流程，然后由 Lean 内核（kernel）检查证明。检查和验证 elaboration 的输出是内核的职责。 Lean 内核是数千行 C++ 代码。内核经过精心设计，但极其复杂。我们前面提到了 mathlib，它由约 250 万行 Lean 语言源代码组成。该库经过了 elaboration，然后由内核检查。如果这 250 万行代码中任何地方存在无条件的假证明，那就是内核或运行时未能拒绝假证明的缺陷。如果底层类型论的缺陷被实现到了代码中，那就是严重的内核缺陷。 Lean 的证明在未经内核检查之前绝不可信。此外，在进行人工审核以确保陈述保真度（statement fidelity）之前，Lean 中的证明不应被接受。被验证的定理是我们所理解的那个吗？Lean 中的定义与我们预期的一致吗？这项任务通常远比检查证明本身简单得多。例如，对于 Navier-Stokes 问题，应当由人工检查 Lean 中的陈述是否对应 Fefferman 对千禧年大奖难题的表述，特别是实数域、偏导数和测度等概念在 Lean 中是否正确定义。Lean 中的比较器工具（comparator tool）可以辅助完成这项任务。该工具还可以执行额外检查，例如检查是否存在未经授权的公理。 **健全性 Bug 之夏** 健全性 Bug（soundness bug）是内核中的一种缺陷，它允许证明"False"，从而证明任何命题。健全性 Bug 是证明辅助器中任何类型缺陷中最为灾难性的，应当引起那些深切关注数学可靠性的数学家的警觉。各种证明辅助器中偶尔会被发现健全性 Bug。2003 年，我在证明辅助器 HOL Light 中发现了一个健全性 Bug，该辅助器当时被认为拥有所有内核中最为可靠的。那个内核非常小，仅由几百行计算机代码组成。对我来说，发现这个健全性 Bug 是一枚荣誉徽章——这是自 1996 年以来该证明辅助器中发现的第一个健全性 Bug。（参见 HOL Light change log，2003 年 7 月。） Lean 4 于 2023 年 9 月发布。发布前发现了两个健全性 Bug 并已修复。2025 年 5 月，另一个由溢出（overflow）引起的健全性 Bug 被报告。2026 年的春季和夏季发生了大规模的混乱，如今被称为"健全性 Bug 之夏"（Summer of Soundness Bugs）。2026 年 7 月和 8 月间发现了多个 Lean 中的健全性 Bug。这场夏季风暴波及了各种证明辅助器，但我聚焦于 Lean。其中一个 Lean Bug 导致了对 Collatz 猜想的非法反证。我是在今年夏天得知这个 Bug 的，当时它在 Lean 中生成了一个开普勒猜想的简短非法证明。所有这些 Bug 都很快被修复，并且 mathlib 已由修复后的内核重新验证。对这些健全性 Bug 的分析可在 de Moura 的[事后分析报告](https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/)中找到。 "Lean 健全性 Bug 之夏"听起来像是一场灾难，但仔细审视会发现，这些健全性 Bug 被发现实际上是一个积极的发展。夏季的 Bug 是由前沿模型 AI 在关注可靠内核的安全研究人员手中被检测到的，而非黑帽黑客所发现。Collatz Bug 由 Ramana Kumar 发现，他是《CakeML: a verified implementation of ML》的合著者之一，该项目创建了一个端到端验证的 ML（函数式编程语言）实现。多个 Bug 由 Dan Selsam 发现。根据 de Moura 的报告，"OpenAI 的 Daniel Selsam 用一个专门针对网络安全的 AI 协助了 Lean FRO，在 Lean 内核中发现了其他编程错误。所有错误均已修复。"与 Selsam 的合作"在内部 AI 报告无法发现更多问题后"结束。Dan Selsam 从 Lean 早期就做出了贡献，是 IMO 大挑战（旨在实现 Lean 中验证的 IMO 级别问题求解）的创建者之一。他最近因关于 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 Bug 就没有被与一个稍显过时的 Nanoda 内核的交叉检查捕获，后者因自身的一个无关 Bug 而接受了非法的 Collatz 反证。计算机芯片可能存在设计缺陷和制造缺陷。还存在软错误、操作系统 Bug 和编译器 Bug。不同的内核可能存在相同的缺陷。其中一些错误可以通过在不同的编程语言、不同的硬件和操作系统上运行不同的内核来缓解。 理想情况下，我们希望对 Lean 内核进行"洁净室"（clean-room）设计——即一个不参考 Lean 4 内核源代码的内核实现，以避免将一个内核中的 Bug 复制到另一个内核。 **2. 形式化验证内核。** **Gödel 不完备性。**我们希望拥有 Lean 4 内核没有 Bug 的形式化证明。然而，Gödel 第二不完备性定理对这一目标施加了严重限制。我们最多只能期望获得一个相对一致性证明。即：如果某某系统是一致的，那么 Lean 4 是一致的；它没有健全性 Bug；它不会产出 False 的证明。 **形式化验证内核有着悠久的传统。**原则上，形式化验证可以同时检查内核的逻辑规范及其具体代码实现；但某些验证可能只检查其中一个而忽略另一个。多年前，John Harrison 在一个加强版的 HOL Light 中形式化验证了 HOL Light 证明辅助器内核的核心部分。这提供了一个概念验证。进一步的改进是上述在 CakeML 中实现的 HOL Light，CakeML 是一种具有形式语义和验证编译器的编程语言。这就是 Candle 项目所做的工作。 还有其他针对不同证明辅助器的重大内核验证项目。 **已验证 Lean 内核之秋** Joachim Breitner 于 9 月 10 日在网上发帖写道