清华姚班校友发起，Claude用11天完成费马大定理首个完整的形式化证明
DeepTech深科技 · 科技资讯
原创 加洋 2026-09-05 09:00 上海 让计算机逐步检查一份复杂的数学证明。 Kevin Buzzard 收到那封邮件时，正在英国威尔士参加音乐节。他的手机信号很差，短暂连上网络后，他才看到一个陌生人发来的标题：“费马大定理的端到端 Lean 形式化”。这位长期研究数学形式化的帝国理工学院教授，把它当成了又一封不靠谱的邮件。 一周后，整理积压的近千封邮件时，他才知道，对方完成了一项什么工作。随后，他编译了代码，运行检查工具，确认检查通过。 9 月 4 日，Anthropic 公布了这项由 其 研究员 彭天翼 （ Tianyi Peng）发起的成果： Claude 在人类少量指导下，用 11 天完成费马大定理的完整形式化证明。 彭天翼 是清华姚班校友，他曾与哥伦比亚大学的合作者开发了数学形式化协作平台 Prove2Me，数十个 Claude 智能体借助该平台协作，生成约 1300 万行 Lean 代码，最终证明使用了约 2.95 万个中间定理。整个过程消耗约 60 亿输出 token。 图丨 Tianyi Peng （来源：Columbia Business School） 费马大定理 本身 早已得到证明。这次工作的新增价值，是把已有证明及其依赖的数学知识，写成计算机能够逐步检查的形式。它展示了 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 曲