Lean 如何工作：一个不信任证明者的程序

9 月 4 日，Anthropic 发布了第一份经计算机检验的费马大定理完整证明。该定理断言：当 n 大于 2 时，不存在正整数 a、b、c 使得 aⁿ + bⁿ = cⁿ。费马大约在 1637 年把它写在一本书的页边，Andrew Wiles 在 1995 年发表了第一个正确的证明，此前人们经历了 350 多年的失败尝试。

Anthropic 并没有找到新的证明。它把 Wiles 的证明（采用 Darmon、Diamond 和 Taylor 阐述的版本）改写成了一种名为 Lean 的语言。完成这项工作的是数十个 Claude 智能体，用时 11 天，期间偶尔有人工提示。结果长达 1300 万行，是 Mathlib 的五倍多。Mathlib 是由社区维护的大型已检验数学库。

没有人会去读 1300 万行代码。尽管如此，伦敦帝国理工学院的数学家 Kevin Buzzard 还是审查了它。他从 2024 年起领导一个社区项目，目标正是形式化同一个证明。他的结论是：这个证明除了数学公理之外不依赖任何其他假设，确实证明了该定理。

五天后，安全公司 Trail of Bits 发布了另一份费马大定理的“证明”。它只有一屏长，而 Lean 同样判定它正确。

两件事都是真的，而理解其中的原因，就是理解 Lean 如何工作。在关于 OpenAI 722 份证明的文章中，我们区分了一个结果“已检验”所涉及的几个层次。这里我们深入第一层：这个程序究竟做了什么，哪一部分必须信任，以及今年这一部分出问题时发生了什么。

能编译的证明

Lean 既是一种编程语言，也是一个证明助手：在这个程序里，证明要写得足够详细，让计算机能够检查每一步。它由 Leonardo de Moura 于 2013 年在微软研究院启动，自 2023 年起由 Lean FRO 负责开发，这是一个为此专门成立的非营利组织。

要理解它做什么，最快的办法是给它两个简单的论断，一个正确，一个错误：

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

错误信息是 type mismatch，即类型不匹配：在需要数字的地方传入一段文本时，编译器给出的也是同样的错误。这不是用词上的巧合。在 Lean 中，一个论断就是一个类型，一个证明就是该类型的一个值。检查一个证明，就是检查这个值是否具有正确的类型，正如编译器检查一个函数是否返回了它声明要返回的东西。

证明与程序之间的这种等价关系，被称为“命题即类型”或 Curry-Howard 对应。逻辑学家们在上世纪三十年代到六十年代之间逐步发现了它，它是 Lean 以及 Rocq、Agda 等其他证明助手的基础。对程序员来说，其后果很容易想象：一个证明正确，就意味着它能编译。

写证明就是与 Lean 对话

几乎没有人手写这些值。通常的做法是使用策略（tactic）：诸如“做归纳”或“用这个等式改写”之类的指令，它们会逐步变换尚待证明的内容。每一步，Lean 都会显示证明的状态：手上有哪些条件，还剩什么目标，后者用符号 ⊢ 标出。

举一个完整的例子：证明在一个自然数的左边加零，结果不变。这看起来显而易见，但在 Lean 中并非如此。加法的定义是沿着第二个数展开的，所以 n + 0 = n 直接由定义得出，而 0 + n = n 则需要证明。

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

有意思的是某一步失败时会发生什么。如果我们跳过重新组合这一步，直接写 rw [ih]，Lean 不会只说一句“不行”：

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

它说明了自己在找什么、在哪里找，以及停在了什么状态。在这种对话中，每一步都会得到即时而精确的回应，这在很大程度上解释了为什么 Lean 已成为做数学的人工智能系统最常用的环境之一。我们稍后会回到这一点。

策略之下是一个程序

策略并不是证明本身，而是构造证明的程序。如果我们让 Lean 显示它以 cero_mas 为名保存的内容，就会看到：

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

这是一个函数，它对每个 n 通过递归、把一串等式连接起来，构造出证明。没有人会这样写，它是由策略生成的。被检查的正是这个对象，它被称为证明项。

这种分离是 Lean 最重要的设计决策。策略可以要多复杂就多复杂。有的策略能独自解决算术问题，比如 omega；有的会搜索已知事实的组合，比如 grind；任何人都可以编写自己的策略。它们都不需要是正确的。它们产生的一切最终都会变成像上面那样的项，而这个项由一个称为内核（kernel）的小组件来检查，内核只知道 Lean 逻辑的基本规则。如果某个策略有错误，构造出了无效的东西，内核就会拒绝它。验证证明的官方指南把策略的错误列为只需编译就已覆盖的情形。

让一套庞大的机制产生结果、再由一个小型检查器审查这些结果，这一思想被称为 De Bruijn 准则，得名于荷兰数学家 De Bruijn，他在 20 世纪 60 年代末的 Automath 系统中将其付诸实践。

这种分离对人工智能至关重要。对 Lean 来说，语言模型只是又一种策略：一个提出步骤的东西。它可能编造一个引理，走上一条荒谬的路，或者生成 1300 万行代码。Lean 不需要信任它，就像它不信任写证明的人，也不信任 omega 一样。

三条公理和一个 sorry

内核接受了某个东西，并不足以说明到底证明了什么。Lean 允许带着空缺和假设工作，而这两者都很容易被忽略。

空缺叫 sorry：一个写在尚未完成的证明位置上的词。Lean 接受它，好让人可以分步推进，但会发出警告并留下记录。假设就是公理，即不加证明而接受的论断。Lean 自带三条公理，常规的数学实践都认可它们，尽管它们的名字不太友好：

• propext：相互蕴含的两个论断是同一个论断。
• Quot.sound：可以把我们视为等价的所有对象当作一个对象来处理。例如，用整数对构造分数时用的就是这种操作，在分数中 1/2 和 2/4 是同一个数。
• Classical.choice：可以从一个非空集合中选出一个元素，即使我们不知道是哪一个。这就是选择公理。

但任何人都可以添加更多公理，包括错误的公理。因此，审查别人的证明时，最重要的命令不是编译它，而是用 #print axioms 询问 Lean 它依赖什么。用我们的例子来看：

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

社区关于如何判断某个结论是否已被证明的指南要求的正是这一点：回应中不能包含这三条公理以外的任何东西。费马大定理的仓库把它变成了编译的条件：

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

写得进页边的“证明”

现在就能理解 Trail of Bits 的把戏了。他们的证明使用了 native_decide。这种策略为了更快，不让内核去做某项计算，而是把它当作编译后的代码来执行。它适合大规模计算，但有代价：除了内核，还必须信任编译器。Lean 会在公理清单中添加一条公理来记录这一点。

某个函数的编译代码有一个错误。从文本中截取片段的那个函数，在对它进行推理和实际执行它时，给出的结果不同。如果从一个大得惊人的位置开始截取片段，它的逻辑定义返回空文本，而编译后的代码却返回整段文本。Trail of Bits 利用这两个结果，得出一段空文本等于一段非空文本的结论。而从矛盾出发可以推出任何东西，包括费马大定理。

编辑器显示了表示“正确”的蓝色标记。但 #print axioms 在三条标准公理之外多列出了一条：flt._native.native_decide.ax_1_1。Trail of Bits 自己也澄清，这不是内核的缺陷。Lean 团队在大约三个小时内修复了最严重的部分，其余部分在五天后修复。这个错误影响 4.33.1 及之前的所有稳定版本，而 Anthropic 的费马大定理仓库用的恰好是 4.33.1。但该项目不受影响：它禁止使用 native_decide，并要求恰好是那三条公理。

教训很实际。判决依据不是编辑器的蓝色标记，而是公理清单。官方指南明确说明：即使定理所依赖的某个部分使用了 sorry，蓝色标记也照样会出现；而名字中带有 _native 的公理，表示部分计算是由编译后的代码完成的。

如果出错的是内核呢？

内核很小，但并非不会出错，7 月的事件证明了这一点。

7 月 25 日，Ramana Kumar 发布了一个借助人工智能得到的考拉兹猜想反驳。这个猜想说：任取一个正整数，若为偶数就除以二，若为奇数就乘以三再加一，如此反复，迟早会得到 1。这个反驳中没有任何 sorry，但它也不成立：它利用了内核在处理嵌套归纳类型时的一个错误。嵌套归纳类型是在其他类型内部用自身来定义的类型，比如一棵树，它的分支是一个由树组成的列表。

7 月 28 日，Kiran Gopinathan 把它归约为一个对“假”的证明，并报告了这个问题。一小时后就有了修复，发布在 Lean 4.32.2 中。费马大定理的证明是用 4.33.1 编译的，已经包含了这一修复。根据 Leonardo de Moura 事后的分析，这个缺陷只能通过元编程触发，也就是通过绕过常规检查、直接向内核提交声明的程序。

最有启发性的是第二重检查。既然内核可能出错，就有了独立的内核：从零编写、重新检查同样这些项的程序。其中最主要的是 nanoda，由 Chris Bailey 用 Rust 编写。Kumar 的反驳也通过了一周前的某个 nanoda 版本，因为它同时利用了 nanoda 的另一个错误，一个与此无关、且已经修复的错误。这需要两个实现中同时存在两个互不相关的错误。De Moura 的结论是，只要两者都使用最新版本，独立检查依然有效。此后，OpenAI 的一位研究者借助一个专门用于安全领域的人工智能，又在内核中发现了更多错误，全部只能通过元编程触发。nanoda 检查器把它们全都检测了出来。

Lean FRO 此前已经在 Lean Kernel Arena 上公开测试各个独立检查器。7 月之后，它在那里加入了针对这些错误的测试，并承诺投资于更多的实现。最引人注目的检查器是 9 月发布的 con-leche：一个外部检查器，附有一份用 Lean 写成的证明，证明它永远不会接受对“假”的证明。它的 README 说明，它由 Claude 实现并证明，由 Lean FRO 的 Joachim Breitner 监督，他形容这些代码是一堆凌乱、但能运行且经过证明的东西。它并没有消除所有的循环性，因为这份证明本身又要由一个 Lean 内核来检查，但一个错误必须同时溜进几个工作方式不同的部分才行。

Lean 官方指南把所有这些检查按严格程度从低到高排列。每一级都增加了保护，但也都留下了一些没有覆盖的东西：

来源：“Validating a Lean Proof”，Lean 参考手册。摘要由 Codin 整理。该指南把最后一级留给高风险场景，例如有奖竞赛，或无法假定其出于善意行事的人工智能系统。

Anthropic 的费马大定理证明通过了最后一级：官方内核；一个 nanoda 版本，它检查了 1,052,234 条声明，没有发现错误；以及 Comparator，这个工具会在隔离环境中验证所证明的陈述与参考陈述完全相同。这不是绝对的确定性，而是另一种东西：信任一个小型、公开、并经过多种方式检验的东西。

没有任何程序会审查的东西

内核保证项证明了所写下的陈述，但不保证这个陈述说的是我们以为的意思。社区指南举了一些例子：可以重新定义什么是自然数，或者把任意一个论断命名为 TheRiemannHypothesis，从而证明某个看似重大定理、实则不是的东西。

费马大定理的陈述是用 Lean 自带的自然数和运算写成的。只有幂运算来自 Mathlib，而 Comparator 会检查它与 Mathlib 中早已存在、经其维护者审查过的陈述一致。因此很容易信任它。仓库本身提醒，没有任何工具能够检查的是：29,511 个中间定理中的每一个，是否都表示其名称所暗示的含义。对最终结果来说，这无关紧要，因为内核会检查它下面的一切。但对一个想从这份证明中学到东西的人来说，这就很重要了。

这正是 Mathlib 最不显眼的作用。截至 2026 年 10 月 8 日，它收录了由 772 人贡献的 290,229 条定理和 137,964 个定义。它的价值不只在于数量：这些是共享且经过审查的定义，基于它们写出的新陈述，读者不必对每个词都心存怀疑。当一个结果需要 Mathlib 中没有的定义时，就必须由该领域的人来审查这些定义，正如我们在讨论依赖自定义定义的 OpenAI 案例时所解释的那样。

为什么它如此适合人工智能

回到开头的那场对话。Lean 对每一步都给出精确的回应，而它的最终判决是一个“是”或“否”，不可能靠听起来有说服力来争辩。对一个人工智能系统来说，它是理想的训练者。在关于是什么让语言模型变得更好的回顾中，我们解释了用可检验的奖励进行训练如何改变了它们的推理方式。Lean 把这个思路推向了极致。

Google DeepMind 的 AlphaProof 是记录最详尽的例子。根据它 2025 年 11 月发表在《自然》上的论文，它通过强化学习学会了在 Lean 中搜索证明，方法受 AlphaZero 启发，并使用了数百万个被自动翻译成 Lean 的问题。它与 AlphaGeometry 2 一起，在 2024 年国际数学奥林匹克竞赛中取得了相当于银牌的成绩。Anthropic 讲述了另一个方向上的类似做法：Claude 在工作时用 Lean 中的部分证明来检验自己的假设，就像它会用数值模拟来判断自己是否走在正确的方向上。

同样的严格性也带来一个令人不安的后果。一个以让 Lean 说“是”为优化目标的系统，只要 Lean 有漏洞，就会找到它们。考拉兹猜想的反驳就是借助人工智能得到的。Joachim Breitner 指出，两个错误几乎同时出现，或许并非偶然：已经有模型能够找到它们。事实上，Lean 官方指南把未经审查的人工智能生成证明，与蓄意欺骗的证明归为同一类。生成系统越强大，检查器就越需要小巧、经过审查并且有冗余。

检查也不是免费的。费马大定理的证明消耗了约 60 亿个输出 token，而且在一个名为 Prove2Me 的协调平台让各个智能体的工作保持有序之前，还经历了几次失败的尝试。重复检查比人工审查便宜得多，但也不简单：据仓库介绍，编译它用 96 个并行进程花了五个半小时，Comparator 则花了将近十五个小时，内存峰值达到 230 GB。

同样的分工，在数学之外

Lean 为数学建立的这种组织方式，已经被用于生产环境中的软件。

在 AWS，Cedar 是一种用来编写授权策略（谁可以对哪个资源做什么）的语言。Cedar 团队为每个组件在 Lean 中维护一个模型，这个模型比实际的 Rust 代码小大约十倍。团队在这个模型上证明安全属性，并生成数百万个随机输入，检查模型和代码给出相同的回应。根据 Lean 发布的案例，如果模型、证明和这些测试没有同步更新，Cedar 就不会发布任何新版本。

在微软，Windows 和 Azure 使用的密码学库 SymCrypt 用 Rust 编写新算法，用一个名为 Aeneas 的工具把它们翻译成 Lean，并证明它们满足从 NIST 标准导出的规格说明。7 月，它发布了首批完整的证明：ML-KEM，一种能抵御量子计算机的密钥交换算法；以及 SHA-3。他们用来解释这项工作的示意图把工作分成三部分。人工智能智能体，他们称之为随机性的，负责编写证明。工具是确定性的，负责编译、翻译和检查。而人则把注意力放在审查标准是如何被形式化的，以及哪些属性真正重要。

这种分工，是 Lean 中对任何把人工智能引入流程的团队最可借鉴的东西，即使这个团队永远不会写一个证明。只要满足三个条件，生成的内容就可以又多又不可靠。负责检查的部分小巧、确定，并且独立于负责生成的部分。确切知道哪些东西被当作了前提，也就是 #print axioms 的对应物：跳过了哪些测试，模拟了什么，什么未经审查就被接受了。人负责审查规格说明，这是任何机器都无法替他们验证的部分。测试和类型系统是同一思路的弱化版本；Lean 则是它的极端版本。

Lean 不信任证明者，无论是人、策略还是模型。我们自己却必须信任某些东西。改变的是它的大小：不再是某位作者的声誉，也不再是长达数年的审稿，而是一个小小的内核、三条公理，以及一个两行就能写下的陈述。有用的问题不再是我们有多信任模型，而是我们最少必须相信什么，以及谁审查过它。

来源

• Anthropic：“Formalizing Fermat’s Last Theorem”，2026 年 9 月 4 日和 anthropics/fermats-last-theorem 仓库，查阅于 2026 年 10 月 8 日。
• Trail of Bits：“A “proof” of Fermat’s Last Theorem that fits the margin”，2026 年 9 月 9 日。
• Leonardo de Moura：内核缺陷 #14576 的分析，2026 年 8 月 1 日和 Lean 4.32.2 发布说明，2026 年 7 月 28 日。
• con-leche：附带一致性证明的 Lean 外部检查器和 Lean Kernel Arena。
• Lean 社区：“Did you prove it?”和 Mathlib 统计数据，查阅于 2026 年 10 月 8 日。
• Lean FRO：历史与组织和 Lean 参考手册：“Validating a Lean Proof”。
• Hubert 等：“Olympiad-level formal mathematical reasoning with reinforcement learning”，《自然》，2025 年 11 月。
• Lean：AWS 的 Cedar 案例和 AWS Open Source Blog：“Lean into verified software development”。
• Microsoft Research：“Verifying Rust cryptography in SymCrypt, from standards to code”，2026 年 7 月 13 日。
• 自编代码示例在 Lean 官方网页编辑器中使用 v4.35.0-rc4 版本测试。