深度 | Claude 11 天「验完」费马大定理：AI 没证明新数学，但把验算工业化了一脚

核心观点：这是协作范式的突破，不是模型智能的突破。真正的产品不是那个 358 年的定理，而是一条能把「十年人力验算」压成「十一天机器验算」的流水线。我判断，自动形式化不可逆，但「谁来审计机器生成的证明」会成为下一个硬问题。

证据等级：[A] 官方/一手 [B] 2+可靠来源 [C] 单一来源 [D] 个人判断

一、先把「证明」和「形式化」分开

9 月 4 日，Anthropic 宣布 Claude 用 11 天完成了费马大定理的「首个端到端、经计算机检查的形式化证明」[A]。新闻标题铺天盖地，但该问的第一句话是：Claude 到底「证明」了什么？

答案是，它没有证明任何新东西。数学上的证明由安德鲁·怀尔斯在 1995 年就完成了，129 页，解决了这个困扰数学家 358 年的猜想。Claude 做的是形式化：把怀尔斯那套「人读得懂、机器验不动」的证明，逐行翻译成 Lean 证明助手能逐步检查的代码 [B]。

这一步的难度不在「想出新想法」，而在「消灭所有跳跃」。人类数学家写证明时会大量省略「显然可得」这类中间步骤，读的人靠直觉补齐；Lean 不吃这套，它要求每个逻辑环节都被机械地、从公理一步步推出来。业界此前普遍估计，把 FLT 完整形式化需要数年乃至十年 [B]。Claude 把预期压缩到了 11 天。

所以定性要清楚：这是一次工程里程碑，不是数学里程碑。 但它真正的价值，恰恰被「AI 证明了费马大定理」这个标题遮蔽了。

上图：359 年的一条时间线。Claude 压缩的是从「有证明」到「机器可验」这最后一公里。

二、11 天 vs 数年：真正的技术突破是 Prove2Me

先把数字摆齐。这次产出了约 1300 万行 Lean 代码，证明了约 30,300 个定理（约 29,500 个中间定理进入最终证明），是 Mathlib 体量的 5 倍以上，成为迄今规模最大的 Lean 证明 [A]。它消耗约 60 亿输出 Token，用的是 Anthropic 内部研究模型，大致相当于 Claude Fable 5.1 [B]。最终证明只依赖 Lean 的 3 条标准公理，定理陈述与 Mathlib 自带的 FLT 陈述完全一致，由 Lean 机械验证通过。

但数字只是结果。真正的技术看点，是它怎么协调数十个 Agent 并行干活。项目由研究员彭天翼主导，他本科毕业于清华姚班，MIT 博士，现为哥伦比亚大学助理教授 [B]。早期的多智能体尝试失败了：Agent 之间丢失项目状态、停止有效协作，一堆并行证明各自为战，拼不成完整证明。

破局的关键是彭天翼和哥大合作者开发的 Prove2Me 平台。它把待证明的定理组织成有向无环图（DAG），每个节点是一个待证中间结论，边是依赖关系。Claude Agent 各领子任务：有的定义概念，有的啃中间引理，有的拼高层命题，谁证完一个节点就更新 DAG，别的 Agent 立刻接上 [B]。这套「依赖图 + 多 Agent 并行」的打法，才是把数年压成 11 天的那根杠杆。

上图：Prove2Me 的依赖图机制，单个 Agent 证明节点、更新 DAG、其他 Agent 接力，是 11 天背后的核心工程创新。

值得一提，它走的不是怀尔斯原版证明，而是 Darmon–Diamond–Taylor 对怀尔斯证明的简化版本 [B]。选一个结构更规整的重述来形式化，本身就是工程判断。

三、1300 万行 Lean：规模本身成了新问题

1300 万行是什么概念？Mathlib，Lean 社区十年积累的核心库，大约 200 万行 [B]。Claude 这一次，11 天，产出了 6.5 个 Mathlib。而 30,300 个定理里，有 29,500 个是「中间引理」：它们不是怀尔斯论文里显式写出的漂亮命题，而是为了补全人类省略的步骤、硬堆出来的脚手架。

这带来一个耐人寻味的问题：当机器生成的证明库以十倍于人类十年积累的速度膨胀，谁来读懂它、维护它、信任它？ 人类数学家不会去读 1300 万行 Lean，他们只看「Lean 编译器通过」这个结果。证明的可信度，从「人读懂了所以信」，转移到了「机器验证器说过了所以信」。

帝国理工学院数学家凯文·巴扎德（Kevin Buzzard）本人就在牵头一个多年的 FLT 社区形式化项目，他做了最硬核的一件事：亲自下载、编译、验证 Anthropic 的仓库，确认它「sorry-free」（没有用 Lean 的占位符作弊）、逻辑成立 [B]。他承认输了这场竞赛，但数学上这成果本质上没有告诉我们任何新东西 [C]。两句话放在一起，就是整个事件最精确的定性：工程上赢了，数学上空的。

上图：三组数字的规模对比。1300 万行代码让「证明库的维护与信任」本身成了新的工程与治理问题。

四、两盆冷水：巴扎德和陶哲轩

两位重量级数学家的批评，比任何标题都更值得认真对待。

第一盆来自巴扎德。他在确认证明成立的同时强调：这是「自动形式化」已有数学的成就，不产生任何新定理内容 [C]。把「形式化」包装成「证明」，就像把「翻译一本外文书」说成「写了一本新书」，翻译可以很有价值，但不是创作。

第二盆更锋利，来自菲尔兹奖得主陶哲轩。他的批评指向更深的隐忧：如果 AI 把所有的试错都内部消化掉，只吐出一个打磨光滑的最终证明，那即使它将来解开了某个开放问题，它对数学几乎不增加价值，因为数学家最珍贵的副产品，往往是那些走不通的路径、失败的尝试和顺带发明的工具 [C]。陶哲轩还亲自辟谣了一个同期谣言，说 Claude 已经解决了纳维-斯托克斯方程，纯属子虚乌有 [C]。这条辟谣本身，就是当下 AI 能力叙事易碎、易膨胀的缩影。

批评之外还有一层归因争议。Anthropic 的仓库大量依赖帝国理工现有的 FLT 项目、Mathlib、第三方工具 Prove2Me [C]。批评者认为「largely autonomous（基本自主）」这个说法高估了 Claude 的角色。而且「11 天、60 亿 Token、数十个 Agent」这些生产过程的描述全是 Anthropic 自述，外部唯一能独立确认的，只是「存在一个有效的、sorry-free 的 Lean 证明」[C]。

上图：把「形式化」和「发现」拆开看，价值与局限都浮出水面。赞誉集中在左上角，争议集中在右下角。

五、真正的大图景：从人力瓶颈转向治理瓶颈

把镜头拉远，FLT 只是自动形式化这条曲线上的一个高光点。

Buzzard、乌克兰数学家 Maryna Viazovska、以及陶哲轩，都是 Math, Inc.「Veritas 计划」的研究员，目标是把现代数学文献大规模形式化 [B]。这个计划已经拿下几个标志性里程碑：强素数定理（约 2.5 万行，3 周完成）、8 维和 24 维球堆积的最优性（约 20 万行，3 周完成）[B]。社区实验「Jacobian Challenge」也证明，开箱即用的 Claude Code 就能产出约 4.5 万行经过验证的 Lean 代码 [B]。

几条线合起来，一个清晰的范式转变正在发生：数学形式化的瓶颈，正在从「人力太慢」转向「治理太难」。 过去十年最大的障碍是没足够的人愿意花数年一行行写 Lean；现在机器能一夜堆出 1300 万行，但新问题来了：谁来审计这些机器生成的证明？语义标签对不对？一个被机器验证通过的巨型证明库，可信度上限在哪里？

Buzzard 给出最乐观的解读：自动形式化是迈向现代数学文献自动形式化的一大步，有希望揪出文献里潜藏的错误、减轻审稿人的负担 [B]。这条价值线是实的。但陶哲轩的担忧同样实：如果形式化的产出是只给结论、不留过程的黑箱，那它验证了正确性，却可能让数学共同体失去从失败中学习的原料。

上图：自动形式化的范式转变。瓶颈从「人力」转移到「治理」，价值线和隐忧线同时被拉高。

六、我的判断

先给结论：「Claude 证明费马大定理」这个标题是错的，「Claude 把费马大定理的验算工业化了一脚」才是对的。

三个我坚持的判断：

第一，这是一次协作范式的突破，不是模型智能的突破。 11 天 vs 数年的差距，不是模型「更会做数学」了多少，而是 Prove2Me 的 DAG 依赖图第一次让数十个 Agent 能稳定并行、接力、不丢状态。我判断，接下来半年「多 Agent + 任务依赖图」会成为自动形式化乃至更广 Agent 工程的标准打法，这个工程的溢出价值比 FLT 本身大得多。

第二，形式化的价值被低估，但「证明」的叙事被高估。 真正会改变行业的是机器验算，让「一个数学结论对不对」从「少数专家花几年读论文」变成「一条命令」。但「AI 证明了费马大定理」这个说法，把一场翻译验证的胜利包装成了发现创造的胜利。

第三，最值得盯的是那个被略过的治理问题。 1300 万行无人能读完的 Lean 代码，意味着数学的可信度第一次大规模从「人」移交给了「机器验证器」。这条线我下判断但不下死注：自动形式化工业化不可逆，但「如何审计机器生成的证明」会成为下一个要解决的硬问题。

一句话：别被「费马大定理」四个字晃了眼。数学还是人的数学，但「验算」这道工序，开始交给机器了。

每日更新。