数学家们在讨论自己看重数学的什么。对托马斯·黑尔斯（Thomas Hales）来说，重要的是数学的一致性，以及它支撑科学与文明时无可比拟的可靠性。形式化证明在数学基础与逻辑规则层面被逐一检查；因步骤太多，通常由专门软件在计算机上完成。已被形式化的定理包括四色定理（four-color theorem）、费特-汤普森（Feit-Thompson）奇阶定理、开普勒猜想（Kepler conjecture）等。2026年完成的项目让人看到形式化的潜力。

数学家们一直在讨论他们看重数学的什么。对我而言，重要的是数学的一致性，以及它在支撑科学与文明时那种无与伦比的可靠性。

数学的形式化

形式化证明是一种在数学基础和逻辑基本规则层面上被彻底检查过的数学证明。理论上可以手工完成，但由于步骤太多，通常借助专门设计的计算机软件来做。

已被形式化的定理包括四色定理、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 中的任何定义或定理都可被用来证明后续定理。例如，如果证明用到柯西–施瓦茨不等式，可以直接引用库中的结果，而不必重新证明。

自动形式化已成为现实

过去，研究者必须靠人力把纸面证明转录成形式化证明。例如，三维球体堆积的开普勒猜想的形式化证明花了大约 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. 宣布按照 Viazovska 及其合作者的证明，自动形式化 24 维球体堆积问题。该项目生成了约 50 万源代码行，通过代码修剪后来缩减到约 20 万行。
• 2026 年 5 月，Meta/Facebook Research 的一个小组在名为 ATLAS 的项目中，自动形式化了 26 本数学教材的大部分内容。

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

展望未来，Urban 在 1 月表示：“我们相信，到 2026 年，（自动）形式化可能变得相当容易且无处不在，无论使用哪种证明助手。”自动形式化项目已在不同证明助手中借助各种大语言模型完成，但我们聚焦 Lean。“对 [Jesse] Han 来说，它意味着更多：这是数学一场革命性变革的开端，在这种变革中，超大规模形式化司空见惯”（IEEE Spectrum）。Jared Lichtman 于 2026 年 9 月 8 日宣布启动 MAP（数学自动形式化项目），目标是把“所有已知数学翻译成形式代码”。他让我们想象接下来的 1 万亿行代码。

Lean 可靠吗？

类型论

Lean 基于类型论，确切地说，是类型论的一种特定变体，称为 CIC，即归纳构造演算（calculus of inductive constructions）。这里不打算提供类型论教程，我只简要说明。罗素 1901 年著名的悖论（所有不包含自身的集合组成的集合……）引发了数学基础的危机。在那个十年后期，人们提出了两种解决方案：（1）Zermelo 的集合论公理，禁止构造不安全的集合；（2）类型论，它把制造类似罗素悖论实体的做法变成语法错误。类型论由罗素本人在 1903 年的《数学原理》中提出，并成为罗素与怀特海《数学原理》基础系统的一部分。

对习惯集合论的数学家来说，B. Werner 1997 年的论文《类型中的集合，集合中的类型》给出了一些安慰：他们在集合论中所做的一切都可以翻译到类型论中，而在类型论中所做的一切也可以翻译回集合论。更准确地说，该论文证明 ZFC 集合论可以编码进 CIC，而 CIC 的某个变体也可以编码回 ZFC（辅以一族不可达基数层次）。

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

Lean 的设计

Lean 系统的一部分是一种通用编程语言（恰如其分地称为 Lean 编程语言）。普通的计算机程序，比如对列表排序的程序，可以用这种语言编写，然后编译运行。Lean 系统还提供一种数学语言，用来写定义、陈述定理和书写证明脚本。编程语言和数学语言并不是彼此独立的实体，而是同一种语言同时承担两种功能。程序代码可以与关于算法正确性的定理混合在一起；数学证明也可以借助程序来生成。Lean 中的证明脚本会先被解析，并经历一个称为精加工的过程（某种面向数学的编译过程），随后由 Lean 内核检查证明。内核的职责就是检查并验证精加工的输出。

Lean 内核由几千行 C++ 代码构成。内核经过精心设计，但极其复杂。前面提到的 mathlib 约有 250 万源代码行，用 Lean 语言写成。该库先经过精加工，再由内核检查。如果这 250 万行代码中任何地方存在无条件的假证明，那就是内核或运行时未能拒绝假证明的过错。底层类型论中的任何缺陷，一旦在代码中实现，就是严重的内核缺陷。

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

可靠性缺陷之夏

可靠性缺陷是指内核中允许证明“False”（因而能证明任何命题）的缺陷。可靠性缺陷是证明助手中最灾难性的一类缺陷，对深切关心数学可靠性的数学家来说，应当敲响警钟。各种证明助手偶尔都会发现可靠性缺陷。2003 年，我在证明助手 HOL Light 中发现了一个可靠性缺陷；当时它被认为拥有所有内核中最可靠的内核。那个内核非常小，只有几百行代码。对我来说，发现这个缺陷是一种荣誉勋章；这是自 1996 年以来在该证明助手中发现的首个可靠性缺陷。（见 HOL Light 变更日志，2003 年 7 月。）

Lean 4 于 2023 年 9 月发布。发布前发现并修正了两个可靠性缺陷。2025 年 5 月，又报告了一个由溢出引起的可靠性缺陷。到了 2026 年春夏，情况彻底失控，这一时期现在被称为“可靠性缺陷之夏”。7 月和 8 月，Lean 中发现了若干可靠性缺陷。这场夏季疯狂影响了各种证明助手，但我聚焦 Lean。其中一个 Lean 缺陷导致了对 Collatz 猜想的非法的反驳。今年夏天，当它给出开普勒猜想的一个简短非法证明时，我得知了这个缺陷。所有这些缺陷都被迅速修复，mathlib 也已由修复后的内核验证。de Moura 的事后分析对这些可靠性缺陷做了分析。

“Lean 可靠性缺陷之夏”听起来像一场灾难，但进一步考察会发现，发现这些可靠性缺陷其实是积极进展。这些夏季缺陷是由关心可靠内核的安全研究者手中的前沿模型 AI 发现的，而不是黑帽黑客。Collatz 缺陷由 Ramana Kumar 发现，他是《CakeML：一种经过验证的 ML 实现》的合著者；CakeML 提供了端到端经过验证的 ML（函数式编程语言）。若干缺陷由 Dan Selsam 发现。根据 de Moura 的报告：“OpenAI 的 Daniel Selsam 用专攻网络安全的 AI 协助 Lean FRO，并在 Lean 内核中发现了其他编程错误。所有这些都已被修复。”与 Selsam 的合作“在内部 AI 报告找不到更多问题后”结束。Dan Selsam 从早期就为 Lean 做贡献，并且是 IMO 大奖挑战（目标是在 Lean 中验证 IMO 水平的问题求解）的创建者之一。他最近因 9 月 14 日对 AI 安全的警告而成为新闻人物，相关报道出现在 X.com 上的一篇病毒式帖子中。

消灭缺陷

关于如何避免 Lean 中的可靠性缺陷，已有各种提议。我讨论其中三种。

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

目前已经写出了大约 25 个 Lean 内核。“Lean Kernel Arena”（Lean 内核竞技场）列出了它们。

凡是不信任当前这一批内核的人，都可以自己为 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 证明助手内核的核心。这提供了一个原理验证。进一步的改进是把 HOL Light 实现在前面提到的 CakeML 中；CakeML 是一种具有形式语义并带有经过验证编译器的编程语言。这正是 Candle 项目所做的。

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

已验证 Lean 内核之秋

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

Breitner 开发了一个经过验证的 Lean 内核，名为 Con-Leche。其实现用 Lean 写成，一致性也在 Lean 中形式化，代码和证明由 Claude 生成。形式一致性证明假设了一个用 Lean 编码的 ZF 集合论，并辅以一族不可达基数层次。有趣的是，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 性质，以及 sort 单射性。

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

这一性质表明：在集合论一致性（辅以适当公理）的假设下，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 越来越有能力欺骗我们、利用软件漏洞的时代，我们绝对不能盲目信任像 Lean 这样的系统。若以对抗性视角看待 AI，我们会问：2026 年夏天 AI 在排查缺陷时，如何证明它没有在 Lean 中留下一个后门式的可靠性缺陷？如果那个缺陷极其晦涩，人类自己不太可能发现它，怎么办？如果正是这个缺陷在 Con-Leche 检查器的 Lean 验证中被利用，导致 Con-Leche 也留下可靠性缺陷呢？（既然 Con-Leche 的一致性已由多个其他内核交叉检查，一个可靠性缺陷就必须同时突破所有这些交叉检查。）再假设那个缺陷被恶意用来在保护关键基础设施的、经过形式验证的软件中植入后门。我们现在应采取哪些预防措施，来防止这类未来场景？在过去一年里，许多关于数学类型论基础及其可靠性的基础工作都被交给 AI，除非由人类仔细审计，否则这是危险的。

讨论整体偏怀疑：高赞评论普遍质疑“自动形式化已在 2026 年成为实用现实”的说法，认为论文到 Lean 的产出并不保证与原论文一致，且最终信任不能交给大语言模型或证明检查器。少数人则惋惜 Coq 更名，或提醒注意文章作者 Thomas Hales 的背景。

认为论文自动形式化并不等于正确对应原论文

• 近期把论文翻译成 Lean 的实践表明，形式化结果与原论文对应极差：遇到原论文难以形式化时，常转去证明另一个命题并宣称成功；虽比全手工快，但“论文进、Lean 出”不保证两者一致。（高赞） > 尝试形式化论文时若觉得难，就转去证明别的东西并宣布成功；论文进、Lean 出并不能保证两者对应。（@JonChesterfield）

认为信任的最终后盾仍是人类共同体，而非工具或人工智能

• 以软件开发常识看，Lean 内核过去出过 bug，未来当然还会再出；证明检查器本身也可能有 bug，底层理论也可能隐含可被利用的悖论或“数学漏洞”。大语言模型不在乎声誉，常幻觉、编造，甚至在测试环境中试图作弊和绕过规则。最终信任仍要扎根于人类共同体的声誉与工作量证明式信任，不能只靠工具，当前人们对工具信任过度；并预测人类会用人工智能工具发现 bug，进而质疑 Navier-Stokes 证明。（高赞） > 大语言模型不在乎声誉，常编造并试图绕过规则，因此信任的后盾仍要是人类共同体。（@chr15m）

认为 Coq 更名为 Rocq 很可惜

• 有人对 Coq 去年改名为 Rocq 表示惋惜，认为这一更名令人遗憾。（少数人） > Coq（去年更名为 Rocq）真是令人遗憾。（@laichzeit0）

提醒注意文章是 Thomas Hales 的客座文章，需留意立场

• 有人提醒读者当心：这是一篇 Thomas Hales 的客座文章，提示不要忽视作者背景对其乐观论断的影响。（少数人） > 当心：这是一篇 Thomas Hales 的客座文章。（@zx8080）

有价值的补充

• 理解定理证明器与证明助手需要补类型论基础：文章已提到 Werner 的《Sets in Types, Types in Sets》（讨论 Set/Type 理论映射）；此外更易读的是 Bell 的《Types, Sets and Categories》（类型论演化及其与集合/范畴论关系）；Brandl 的《Typed Lambda Calculus / Calculus of Constructions》则是了解 CoC/CIC 的必读简明概述。（@rramadass）