Claude 11 天验完费马大定理，数学家却说没多出一点新东西
8 月 17 日深夜，美东时间，一个叫 Prove2Me 的平台上，费马大定理的根节点状态跳成了 PROVED。系统日志里有一条来自执行任务的 AI 自己写的话，“这场行动的历史性时刻（待复核）”。
半个多月后，Anthropic 在 9 月 4 日发布了官方文章，把这件事讲完整。Claude 用 11 天，基本自主地完成了费马大定理的 Lean 形式化证明，约 1300 万行代码，是 Lean 最大的数学库 Mathlib 的五倍多，顺手成了人类迄今造出的最大的数学证明。
我把能找到的材料对了一遍，Anthropic 的官方文章、公开的代码仓库，还有 Kevin Buzzard 的公开说法。Buzzard 是帝国理工的数学家，主持着人类这边干同一件事的项目。能确认的事实先讲清楚，掺了我自己判断的地方会单独说。
先说清这是件什么事
Claude 没有发明新数学。这句话是理解整件事的起点。
费马大定理说，n 大于 2 时，aⁿ+bⁿ=cⁿ 没有正整数解。1637 年费马在一本书的页边写下这个断言，还说自己有个绝妙的证明，页边太小写不下。这一等就是 358 年。怀尔斯 1993 年 6 月讲完三场讲座，审稿人在原稿里发现了漏洞，他和学生 Richard Taylor 又补了将近一年，1995 年才正式发表，129 页。
129 页的证明，数学界审了几个月才敢信。形式化是另一条路，把证明的每一步翻译成 Lean 这类证明助手能逐行机器检查的语言。检查只依赖三条基础公理，不需要信任任何人的名声。麻烦在于翻译量。人类论文里一句“显然可得”，Lean 要求你把“显然”展开成一行行代码。帝国理工的 Buzzard 从 2023 年底开始带队做这件事，英国研究理事会拨了 93.4 万英镑，项目期排到 2029 年 9 月，光路线蓝图就写了 86 页。
Anthropic 此前预计，费马大定理的形式化要干好几年。
第一轮是怎么失败的
Anthropic 的第一轮尝试没有成功。几十个 Claude 智能体并行开工，干着干着就丢了状态，忘了谁证过什么，重复劳动，有的还建立在尚未证好的定理之上。这些失败的尝试后来贡献了最终证明里约 7% 的非模板代码行。
翻盘靠的是换平台。Prove2Me 由 Peng Tianyi 和他在哥伦比亚大学的合作者开发，用一张有向无环图记下全部定理和它们的依赖关系，每个智能体随时能查哪些已经证完、下一步该证什么；定理陈述和证明分开存放，编译不用互相等待；每个定理还配一段自然语言描述，可以搜索，可以复用。
Peng 是清华姚班 2017 届本科，MIT 博士，现在是哥大助理教授。整个 11 天里，人类的参与主要是他偶尔丢进来的几句话，其中一条是“Jacobian as a scheme 听起来优先级很高”。
最终这轮跑完，几十个智能体消耗了约 60 亿输出 token，证明约 30300 个定理，其中 29500 个进入最终证明。Lean 检查通过，只用三条标准公理，代码里没有一条 sorry，那是 Lean 里“这步先欠着”的占位符。仓库里 106 个文件直接复用了 Buzzard 项目和 flt-regular 项目的成果，n=3 和 n=4 两种情形干脆取自 Mathlib。
Buzzard 亲自编译复核了这份证明。他给了两句评价，一句是“非凡的自动形式化成就”，另一句写在他博客的标题里，费马大定理，Anthropic 抢在我前面了。
脚手架比模型值钱
下面是我的判断。
两轮尝试用的是同一个模型。第一轮失败，第二轮成功，中间换掉的只有平台。做过工程的人对这一幕不会陌生，单个工人再强，没有一块所有人都能看见的任务板，几十个人就会互相踩脚。这次真正的突破在于，把共享记忆做成了基础设施，几十个智能体才有可能拼出一件任何单个智能体都撑不完的长活。这个信号对眼下所有做多智能体系统的团队都适用，值得把它排在任何新模型发布会前面。
第二笔账是钱。60 亿输出 token，按 Claude Fable 5.1 公开的输出价格粗算，50 美元一百万 token，大约 30 万美元。Buzzard 的项目拿了 93.4 万英镑，计划干到 2029。这笔账要算得诚实，两边不完全可比，人类项目在从零定义数学结构，Claude 站在人类 106 个文件的肩膀上，那 1300 万行里也有大量冗余，Anthropic 自己都说它很可能远比需要的长。但价格差了三倍还多，时间差了三年，这种量级的差距，历史上一般不会往回走。
数学没多，信任的造法变了
Buzzard 说得直白，数学上，这项工作几乎什么都没告诉我们。费马大定理 1995 年就证完了，形式化不产生新定理。
它动的是另一头。数学成果的可信度，过去来自审稿人几个月的阅读。黑尔斯 1998 年证明开普勒猜想，评审拖了多年，最后只给出“高度可信”的说法。当 AI 开始批量产出数学结果，人读不过来是迟早的事，机器检查可能是唯一跟得上的办法。
Anthropic 顺手做了一个小实验。三个个人 Claude Max 订阅，通过同一个平台协作，三天完成了 Vinogradov 三素数定理的形式化。消费级订阅，三天。这件事的成本门槛已经低到数学系研究生宿舍凑一凑能够到的程度。
以后论文大概会一式两份，人读一份，机器验一份。审稿人不会失业，工作却会改道，从逐行核对这步对不对，转向判断这个问题值不值得证。
费马当年在页边留下的遗憾，缺的是一个能验证那句话的办法。这个办法现在有了，造它只花了 11 天。
主要来源包括 Anthropic 官方博客 Formalizing Fermat Last Theorem，Kevin Buzzard 的博客与帝国理工 FLT 项目页，以及 IT之家、腾讯新闻的相关报道。