清华姚班校友发起，Claude用11天完成费马大定理首个完整的形式化证明|怀尔斯|数学|清华|费马大定理

Kevin Buzzard 收到那封邮件时，正在英国威尔士参加音乐节。他的手机信号很差，短暂连上网络后，他才看到一个陌生人发来的标题：“费马大定理的端到端 Lean 形式化”。这位长期研究数学形式化的帝国理工学院教授，把它当成了又一封不靠谱的邮件。

一周后，整理积压的近千封邮件时，他才知道，对方完成了一项什么工作。随后，他编译了代码，运行检查工具，确认检查通过。

9 月 4 日，Anthropic 公布了这项由其研究员彭天翼（Tianyi Peng）发起的成果：Claude 在人类少量指导下，用 11 天完成费马大定理的完整形式化证明。彭天翼是清华姚班校友，他曾与哥伦比亚大学的合作者开发了数学形式化协作平台 Prove2Me，数十个 Claude 智能体借助该平台协作，生成约 1300 万行 Lean 代码，最终证明使用了约 2.95 万个中间定理。整个过程消耗约 60 亿输出 token。

图丨Tianyi Peng（来源：ColumbiaBusinessSchool）

费马大定理本身早已得到证明。这次工作的新增价值，是把已有证明及其依赖的数学知识，写成计算机能够逐步检查的形式。它展示了 AI 处理大型数学形式化工程的能力，也为一个越来越现实的问题提供了工具：当 AI 生成的数学证明越来越多，谁来确认它们是对的？

费马大定理的表述很简单：当整数 n 大于 2 时，不存在满足 aⁿ＋bⁿ＝cⁿ 的正整数 a、b、c。费马大约在 1637 年写下这个断言，数学家花了 350 多年才完成证明。

1993 年，安德鲁·怀尔斯通过一系列讲座公布了证明。此后数月的审查中，一位审稿人的提问暴露出关键漏洞。怀尔斯又花了一年多时间，最终与理查德·泰勒合作补上缺口，相关论文于 1995 年发表。

这段经历表明，不论是找到证明路径，还是确认每一步推理是否严密，都需要投入大量工作。传统的数学论文通常面向同行写作，往往会省略读者有能力补齐的推导步骤，直接引用其他文献的结论，有时还依赖领域内约定俗成的知识。因此，审稿人核查一项复杂结果时，需要沿着这些引用和推导追溯很长一段逻辑链条。

而像 Lean 这样的证明助手，则将核验工作交由计算机执行。

它采用“命题即类型”的设计：命题规定一个类型，证明则是符合这个类型的对象。模型可以通过代码和自动化策略寻找证明，最终仍需生成一个由 Lean 核心程序检查的证明项。

例如，要证明“如果 A 成立，那么 B 成立”，就需要构造一种方法，把 A 的证明转换成 B 的证明。Lean 检查这个构造是否符合逻辑规则。这让生成证明与核验证明可以分开：即使负责生成代码的模型经常出错，只要检查环节可靠，错误就不能成为被接受的最终证明。

费马大定理的难点，在于需要把极长的推理链及其依赖的数学知识，一起放进这个系统。Claude 沿用了怀尔斯与泰勒相关工作的证明路线，主要参考 Darmon、Diamond 和 Taylor 的阐述。

这条路线采用反证法。假设费马方程存在一组反例，经过约化，可以集中处理素数指数，并用反例构造一条特殊的椭圆曲线，即 Frey 曲线。怀尔斯的工作保证这类半稳定椭圆曲线具有“模性”，意味着它的算术信息能够与模形式对应。

接下来，Ribet 的降层结果把相关模形式的层数降到 2，迫使一个权为 2、层为 2 的非零尖点形式存在。但这样的形式并不存在。矛盾由此产生，最初假定的费马方程反例也就不能存在。

把这段推理交给计算机，需要补齐每个环节成立的条件。公开代码将其拆为反例约化、Frey 曲线构造、相关伽罗瓦表示的不可约性、模性、降层，以及最终的尖点形式空间为零等部分。

其中，伽罗瓦表示把数域的对称性编码为矩阵作用，是连接椭圆曲线与模形式的重要工具。模性证明还用到了“3—5 切换”：先研究曲线上与素数 3 有关的表示；当这一支不满足所需条件时，借助另一条曲线和素数 5 的表示完成转接。这里的 3 和 5 是证明工具，与费马方程中待处理的指数作用不同。

这也解释了 Anthropic 公布的日志中，为什么会出现“R＝T 完成后，结果一路传到根节点”的记录。

R 与 T 是模性提升论证中的两个代数对象：R 描述满足指定条件的伽罗瓦表示变形，T 则来自模形式上的 Hecke 算子。证明两者之间的自然映射是同构，就能在相应条件下把表示与模形式连接起来。这样一个中间环节完成后，依赖它的更大结论才能接续成立。

需要注意的是，项目中所谓的“完整证明费马大定理”，有着明确的工程范围定义：系统只需要把沿途涉及的经典定理证明到“足以支持当前最终目标”的程度。例如，它证明了 Frey 曲线所需的不可约性，以及特定条件下的降层结果；这不等于完成了 Mazur 或 Ribet 相关定理所有一般版本的形式化。较小指数还通过下降法、正则素数情形的已有形式化成果等分支处理。

这些相互连接、难度不同的任务，构成了多智能体协作的对象。

Anthropic 最早的尝试并不顺利。智能体虽然各自证明了一些结果，却逐渐无法准确掌握整个项目的状态，协作随之失效。团队转向 Prove2Me 后，用平台维护的定理依赖图记录进展，减少对模型对话记忆的依赖。

Prove2Me 的关键设计，是将定理陈述与证明分开保存。定理陈述一旦提交便固定下来，不同智能体可以针对同一个目标寻找不同证明。这样，一个智能体修改证明方法时，其他智能体所依赖的命题不会跟着变化。

平台还允许提交“证明草图”：先严格证明目标如何依赖若干子定理，把子定理的证明留给其他任务。比如，一个智能体证明“只要 A、B、C 成立，D 就成立”，另外三个智能体分别处理 A、B、C。前一个智能体提交的是已经由 Lean 检查的逻辑连接，而不仅是一份自然语言计划。

此时，D 仍然只是有条件成立。只有它依赖的子定理及其更深层依赖全部补齐，才能组成完整证明。这种拆分可以反复进行，把大型目标变成许多能够独立处理的任务。

Anthropic 介绍，平台同时维护每个定理的自然语言说明，方便智能体搜索和复用已有结果；将陈述与证明分成不同文件，也有助于减少编译开销。对包含数万项中间结果的工程来说，搜索已有成果、避免重复劳动，与继续生成代码同样关键。

最终，数十个 Claude 智能体通过基于 Claude Code 的协作框架完成任务。整个过程中证明了约 3.03 万个定理，最终证明使用了其中约 2.95 万个。人类的数学指导主要是偶尔调整优先级，例如要求尽快推进某项关键定理。

但一份 Lean 工程能完成构建，仍不足以单独支持“费马大定理已经得到完整核验”的结论。还需要检查：有没有把未证明的内容当作前提，以及最终证明的命题是否准确。

Lean 允许开发者用 sorry 暂时跳过一个证明，继续编写后续内容。这个占位符会引入特殊公理 sorryAx。如果最终证明依赖它，就意味着推理链上仍有缺口。因此，核验必须沿着依赖关系检查全部公理，不能只看最后一个文件是否报错。

此次项目披露的最终依赖只有三个常用数学公理：propext、Classical.choice 和 Quot.sound。它们分别涉及逻辑等价命题的相等、从非空类型中选择元素，以及等价关系下的商对象。它们属于 Lean 数学推理的基础，并没有把费马大定理或某个关键数论结论预先设为真。

另一项风险是“证明了错误的目标”。假如模型把题目悄悄缩小为某几个指数，或增加了不合理的前提，Lean 仍可能接受这个被改写后的命题。检查程序能保证形式推理成立，却不能仅凭一个定理的名字判断它是否忠实于原意。

Anthropic 因此使用 comparator，将最终命题及其引用的定义与 Mathlib 中的费马大定理进行比对，并重新通过 Lean 核心检查证明。团队还把证明环境导出，交给另一个以 Rust 编写的独立核心 nanoda 核验。项目披露，nanoda 在核验中接受了超过 105 万项声明（该数字包含导出的整个运行环境，不能与项目中提取的约 2.95 万个核心定理直接等同）。

为了完成检查，团队对 nanoda 做了四处补丁，其中一处增加进度显示，三处改善检查性能；据项目说明，这些修改没有改变类型检查规则。多套检查增加了核验依据，结果仍建立在逻辑基础及检查程序正确实现的前提上。

必须指出的是，“证明通过机器检查”与“证明适合人类阅读和复用”，属于完全不同的工程目标。

Anthropic 承认，约 1300 万行代码超过 Mathlib 规模的 5 倍，部分原因是 Mathlib 长期经过整理和审查，而这份证明可能比实际需要的长。模型生成了可以被机器检查的结果，进一步压缩代码、统一定义、整理可复用模块，仍需要投入工作。