2026 年 9 月 4 日，Anthropic 宣布了一个令学术界震动的消息：几十个 AI 智能体仅用 11 天，就完成了费马大定理的完整机器验证。作为对比，帝国理工学院的顶级数学家团队拿了 100 万英镑的经费，为同样的任务排期了整整 5 年。
这个困扰人类 350 多年的数学悬案，早在 1995 年就被人类天才安德鲁·怀尔斯（Andrew Wiles）证明了。今天这场 11 天对决 5 年的战役，颠覆的并不是数学本身的边界。
这场对决真正摧毁的，是依赖人类专家来建立知识信任的陈旧模式。一篇顶级论文从「人类同行审阅数年且可能出错」，变成了「机器几分钟跑通逻辑断点」。
350年悬案暴露人类评审弱点
回看费马大定理的证明史，简直是一部人类审查系统不断崩溃的记录。1908 年德国悬赏 10 万金马克征集证明。重赏之下，第一年组委会就收到了 621 份看似严密的解答，结果无一例外全被查出致命错误。
人类大脑在处理巨量复杂逻辑时，先天存在盲区。1993 年 6 月，怀尔斯在剑桥牛顿研究所连开三场讲座，向全世界宣布自己证出了费马大定理。然而两个月后，审稿人在常规检查中问出了一个尖锐问题，直接暴露了证明框架中的一个致命漏洞。
怀尔斯为此又花了一整年时间痛苦修补，甚至一度想要放弃，直到 1995 年 5 月才将长达 129 页的最终论文正式发表。依赖几个顶级大脑在小黑屋里审查一百多页密密麻麻的手稿，这种手工作坊式的验证方式，当时已经逼近了人类认知的物理极限。
图：Anthropic 官方发布页头图。来源：Anthropic
11天写出1300万行机器代码
如何让机器来验证一堆晦涩的数学符号？这就需要「形式化」：把一篇极具跳跃性的人类散文式证明，翻译成连标点符号都不许错的机器代码。在过去，这是只有狂热信徒才会做的苦力活。
帝国理工学院的 Kevin Buzzard 教授原本牵头了一个社区项目，计划用 5 年时间来完成费马大定理的形式化。他们光是写一个指导翻译路线的「蓝图文档」就写了 86 页。
Anthropic 的内部研究模型 Claude 在 Prove2Me 平台上，把这个漫长的日历压缩到了不到两周。它不仅沿用了 1995 年经典的简化论证路线，还生成了多达 1300 万行代码。这个体量是当前该平台官方数学库所有代码总和的 5 倍多。
代码中包含了 30300 个定理的证明过程，最终用上了 29500 个。几十个 AI 智能体像不知疲倦的齿轮一样并行协作，把模糊的人类直觉强行掰碎，塞进机器能逐句执行的逻辑链条中。
30万美元买断绝对确定性
工业级算力的介入，让原本高昂的人力成本变成了直接的算力账本。Buzzard 团队的 5 年计划耗资 100 万英镑，依赖的是人类科学家的脑力、薪水和漫长的沟通成本。
而 Claude 的这次验证，消耗了约 60 亿个输出 token。按照目前的公开 API 价格估算，这笔账单大概在 30 万美元左右。用 30 万美元算力换取 5 年人力才能沉淀的绝对确定性，前沿探索的成本结构在这里发生了不可逆转的重构。
机器并非从不犯错。早期尝试中，智能体们曾陷入协作失效，丢失了项目状态。但系统迅速在试错中调整，失败的尝试最终贡献了最终代码约 7% 的非样板行。Anthropic 的研究员只需要在最顶层下达指令，剩下的排雷工作全交给了机器自行消化。
图：Prove2Me 平台上的证明路线 DAG 图，展示 Claude 如何拆解子定理逐层逼近 FLT。来源：Anthropic
科学信任机制移交给了编译器
Kevin Buzzard 教授亲自验证了这份长达千万行的代码，编译器顺利通过。对比工具也确认所有定理陈述与已知数学库完全一致。这也宣告了一份有 20 年历史的「100个形式化挑战」基准测试清单正式清零收官。
正如 Buzzard 自己所说，数学上并没有发现新东西，但在自动化形式化领域，这件事提供了一个强烈的实证。当长达 129 页的数学证明可以像普通软件工程的源代码一样被编译时，学术界的信任网络就被彻底替换了。
过去，大家相信一个定理成立，是因为几位泰斗级人物背书。如今，这种中心化的权威节点被瓦解了。只要代码能够跑通编译器，真理就不需要任何人的担保。人类不再需要提心吊胆地寻找逻辑裂缝，编译器接管了这道最终防线。
参考链接：
- Anthropic Research
- HN 讨论
