Claude用11天写下1300万行Lean代码，费马大定理首次有了机器可核验的完整证明

2026-09-07 11:22:05

费马大定理终于有了第一份能被计算机从头检查到尾的完整证明。据Anthropic公布的信息，Claude在11天内基本自主完成整个工程，写下约1300万行Lean代码，沿途证明了29500多个中间定理。项目由Anthropic研究员Tianyi Peng发起，他在哥伦比亚大学的团队长期从事AI形式化工具开发。相关成果已在GitHub公开，采用Apache 2.0许可。

这项工作的性质需要说清楚：Claude没有提出新的证明路线，它做的是把已有证明转写成机器能够逐步核验的形式。费马大约在1637年在《算术》一书的页边写下那个著名判断——当整数n大于2时，不存在满足aⁿ+bⁿ=cⁿ的正整数a、b、c——并留下一句”页边太窄写不下”。此后350多年间，1993年安德鲁·怀尔斯在三场讲座中公布证明，两个月后审稿人发现关键缺口，他与理查德·泰勒又花近一年修补，1995年才发表长达129页的完整证明。数学界此前普遍预计，把怀尔斯的证明完整形式化需要数年时间。

工程细节更具参考意义。据Anthropic披露，数十个Claude智能体协作，基于Claude Code框架运行，使用的是与Claude Fable 5.1大致相当的内部研究模型，全程消耗约60亿输出token。最初的尝试失败了——智能体会丢失项目状态、协作失效，研究团队改用Tianyi Peng与哥伦比亚大学合作者设计的开源平台Prove2Me后才取得突破。Prove2Me维护一张定理语句的有向无环图，让智能体选择下一个可攻击的节点，把语句与证明分文件存放以减少重编译，并为每条语句保留自然语言描述以便检索复用。有意思的是，失败尝试贡献了最终证明中约7%的非样板代码。

核验结果的严谨度是这则消息的重点。最终证明只依赖Lean的三个标准公理——propext、Classical.choice和Quot.sound，不含axiom、sorry、unsafe等”走捷径”的语句，规模超过其所基于的Mathlib库五倍以上。除Lean自身外，团队还用Rust编写的独立内核nanoda 0.4.13检查了1052234条声明，未发现错误；帝国理工学院数学家Kevin Buzzard也自行编译确认。Buzzard自2024年起发起用Lean形式化费马大定理的社区工程，项目第一阶段技术蓝图就有86页。

Buzzard的评价保持了学者的克制。他在9月4日发文称”Anthropic抢在了我前面”，并指出：”从数学上说，Anthropic的这项工作基本没有告诉我们新东西——我早就说过我有99.9%的把握认为费马大定理的证明是对的。”他同时肯定，”AI自动形式化的产物现在已经足够健壮，可以作为基础继续构建；这个证明是多层的”。Anthropic也在公告中明确划线：与近期产生新数学的黎曼猜想工作不同，这里的新意在于”验证”。当AI产出越来越多的证明，能轻易把它们形式化，将大幅减轻评审新结果的负担——这一过程过去往往要耗时数月甚至数年。

放在行业背景下看，这则消息是本周AI密集更新的一个切片。据CNBC报道，Anthropic率先在周二发布Claude Fable 5.1和Mythos 5.1，随后Meta、谷歌相继推出模型升级，OpenAI紧接着发布GPT-6 Astra，更新节奏之快让企业CIO不得不投入大量资源比较不同产品的价格与能力，”模型疲劳”的说法开始出现。Gartner预计，2026年全球AI支出规模将达2.59万亿美元，较2025年增长47%。在数学方向上，Anthropic一个月前曾用Claude发现黎曼zeta函数的新信息，OpenAI上月则宣称用Astra模型解决了若干个Erdős问题。此外，Anthropic在另一组实验中用三个个人版Claude Max订阅，在三天内完成了维诺格拉多夫三素数定理的形式化，暗示协同形式化的门槛可能比想象中更低。