FRONTIER · 落到现实

怀尔斯的 129 页证明，人验了几个月；Claude 用 11 天写了 1300 万行 Lean——这次被自动化掉的不是证明，是审稿

Formalizing Fermat's Last Theorem

Tianyi Peng 与 Anthropic 研究团队 牵头人在哥伦比亚大学的课题组专做 AI 形式化工具，并设计了本次赖以成功的开放协作平台 Prove2Me；产出是迄今最大的 Lean 证明——1300 万行、29,500 条定理，经 Lean 内核、官方工具 comparator 与独立 Rust 内核 nanoda 三重复核，并由帝国理工 FLT 形式化项目负责人 Kevin Buzzard 审读

2026 年 9 月

为什么选它AI 做数学吵了两年，争的都是「它能不能想出新东西」。这篇掉了个头：新数学怀尔斯 1995 年就给了，瓶颈是没人验得动。最贵的那道验证工序 11 天做完，且可被第三方从头重跑，交付清单别处拿不到。

9 月 4 日，Anthropic 放出了费马大定理的第一份完整的、机器逐步核对过的证明。费马 1637 年在书页空白处写下那句「我发现了一个真正美妙的证明，可惜这里太窄写不下」，怀尔斯 1995 年把它证了出来，129 页，几位数学家验了几个月——中间还被审稿人问出一个致命缺口，怀尔斯又补了一年才堵上。把这份证明翻译成计算机能逐条核对的形式，这个想法二十年前就有人提，2024 年 Kevin Buzzard 在帝国理工正式立项，光是描述第一阶段的蓝图就有 86 页，原本预计要干好几年。Claude 花了 11 天。

但值得读的不是「AI 证出了费马大定理」。它没有证，它是把怀尔斯的证明重写了一遍——跟的是 Darmon、Diamond、Taylor 那版简化讲义，还直接接手了帝国理工项目和 flt-regular 已经写好的 Lean 代码。新东西在另一头：这次被自动化掉的是「验」，不是「证」。数学界最贵、也最没人愿意干的一道工序——一个人读懂另一个人几百页的长证明、并确认它没塌——第一次被机器整块吃了下去。第 24 篇里陶哲轩担心的那场「证明过剩、消化不良」，这是目前对它最正面的一次回应。

为什么「验」比「证」更难

Lean 是一种证明助手：你把证明写成它认得的代码，它的内核逐条核对每一步是不是真的从公理和已证结论推出来，全过了，就等于机器给你背书。麻烦在于，人写给人看的证明会跳过大量「显然」，Lean 一步都不让跳；人还可以随手引用几百年的文献，形式化却只能站在「已经被形式化过的那一小块数学」上往前搭。

验证有多贵，Anthropic 在脚注里排了一串例子：Hales 1998 年的开普勒猜想证明审了四年，12 人评审组最后只肯给「99% 确定」，Hales 只好又拉二十个人做形式化；佩雷尔曼 2002 年的庞加莱猜想证明，数学界花了大约四年、写了三份三百页的详解才接受；Helfgott 2013 年的弱哥德巴赫猜想证明至今还挂在评审里。也有反过来的：错的结果被当成对的用了很多年，后面的理论就建在坏地基上。1908 年有人给费马大定理悬赏十万金马克，光第一年就收到 621 份错证。证明的产量从来不是瓶颈，判断它对不对才是。

11 天，1300 万行，29,500 条定理

牵头的是 Tianyi Peng，Anthropic 的研究员，他在哥伦比亚大学的组本来就在做 AI 形式化工具。他起初只想看看 Claude 能不能推进一点，结果一路推到了终点：11 天写出 1300 万行 Lean，证出 30,300 条中间定理（最终证明用到其中 29,500 条），代码量是 Mathlib（社区维护的数学定理主库）的五倍多。这个五倍不是褒义——Anthropic 自己在脚注里写，Mathlib 简洁且被反复审过，而「我们的证明很可能比它需要的长得多」。

人类的输入少到什么程度：Peng 偶尔丢一句高层指示，比如「Jacobian 当成 scheme 来做，优先级看着挺高」「把 Mazur 那条推快点」。算力那一侧则不便宜——约 60 亿个输出 token，用的是一个未发布的通用内部研究模型，Anthropic 说大致相当于 Claude Fable 5.1。

第一次是失败的，救场的不是模型

最初几轮尝试全垮了，描述很具体：agent 一开始也能出活，但很快就搞不清整个项目进行到哪一步，也不再有效地互相配合——那几轮的产出只占最终证明非样板代码的约 7%。转机来自换掉协作方式，用上 Prove2Me——Peng 和他哥伦比亚的合作者做的一个开放形式化协作平台。它干了三件事：把所有待证命题维护成一张有向无环图，agent 从图上挑下一个该证的目标；把「命题陈述」和「证明」拆进不同文件、只单独维护它们之间的链接，于是 Lean 编译快了、资源省了；再给每条命题配一段自然语言说明，让后来的 agent 搜得到、用得上。

这三件事没有一件是数学。它们全在解决同一个问题：一群 agent 长时间干一件大事时，会忘记自己在干什么。那张有向无环图本质上是把项目状态从模型的上下文里搬到了外部，让记忆退化不再致命，顺便让并行成为可能——和第 15 篇讲的上下文工程是同一个调子。另一个佐证是成本：换上 Prove2Me 之后，Anthropic 的研究员用三个个人版 Claude Max 订阅，三天就合作形式化了维诺格拉多夫三素数定理。

它把「怎么复核」也一起交了出来

这份成果的验收材料做得比正文还密。GitHub 仓库的默认构建目标里写死了一条断言：主定理只依赖 Lean 的三条标准公理，多一条、或者有任何一处 sorry（占位符，意思是「这里先欠着」），构建就直接失败。全仓 60,475 个模块从零编译通过；官方工具 comparator 再做一遍独立核对，确认被证的那条命题和「只用 Mathlib 写出来的费马大定理」逐字一致——这是整套设计里最要紧的一步，因为形式化最容易出的错不是证错，是把定理写歪了再去证一个更弱的东西。此外还有第二个内核：nanoda，一个用 Rust 独立实现的 Lean 内核，重新检查了导出的 1,052,234 条声明，无错。

代价也一并公开：重跑一遍构建，96 并发下 5 个半小时，内存峰值 153 GB；comparator 那一遍 15 小时，得留 300 GB 内存。而 README 里最诚实的一句留在最后：没有任何工具能检查每条中间定理是不是真如它的名字所说——名字是机器生成的，「名字和陈述打架时，以陈述为准」。

把它当数学突破读会读错，它是一道工序被自动化的新闻。费马大定理三十年前就被证明了，这次没有一行新数学；真正变了的是「机器已核对过的部分」和「人读过的部分」之间的比例——1300 万行里人读过的接近于零，而机器把每一行都过了两遍内核。这个状态在数学里是全新的。它的可信度全压在一个点上：被证的那条命题，是不是我们想证的那条。Anthropic 显然知道这是唯一的死穴，所以才有 comparator 那一步——拿一份只用 Mathlib 写的费马大定理陈述去逐字比对，确认不是证了个更弱的表亲。这一步做得干净，我认为是整件事里最值得别的团队抄走的设计。但顶上那条命题被对上了，底下 29,500 条中间定理仍然没人读得懂，仓库自己也承认没有工具能保证它们名副其实。于是我们拿到的是一个二值答案：对。没有理解，没有洞见，没有「原来如此」。这不算缺陷，是这类产物的形状——Anthropic 自己也强调形式化不该取代写给人读的叙述。还有一处细节值得留意：Buzzard 的评价里带了一句限定，「Anthropic 的研究者说这只花了 11 天」。他为产物背书，没有为过程背书，这个分寸是对的，因为 11 天这个数字目前只有一方能核。至于能推广到哪，我的判断和第 52 篇是同一条：这套办法只在有标尺的地方管用。Lean 就是那把标尺，它能无情地告诉每个 agent 这一步对不对，所以几十个 agent 才敢并行地试、失败、重来——第 30 篇里那个把实验一条不落跑完、论文却被原作者判 Strong Reject 的例子，缺的正是这把尺。反过来说，最难的那件事——先得有一个正确的证明——这次是怀尔斯 1995 年就给好了的。真正该盯的下一个信号，是有人拿这套流程去形式化一份还没人敢确信的证明，并且从里面抓出错来。

数学形式化验证Lean多智能体科研自动化

去读原文 本文是原创导读，不是原文翻译——真正的细节、证据和微妙之处都在原文里。原文Anthropic 研究博客 · Formalizing Fermat's Last Theorem → 原文Lean 4 证明仓库 · anthropics/fermats-last-theorem（含 PROOF-PATH.md 与可离线浏览的证明网页）→ 原文Prove2Me 论文 · An open collaborative platform for scaling math formalization（本次协作靠的平台）→

上一篇在开源模型上用梯度练出的一串乱码，贴到闭源模型后面照样管用——而最好的那道防线，只把成功率从九成压到四成下一篇参数、算力、KV 缓存三样一分不许多花，让中间一半的层再跑一遍——省下 15% 训练算力，而第二遍干的是把注意力从句首那个黑洞里拽回来

本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。篇目由编辑独立选取，来源均经人工核实。