Claude 把费马大定理完整形式化了：1300 万行 Lean，11 天

9 月 4 日，Anthropic 发布了费马大定理的第一个完整机器验证证明（https://www.anthropic.com/research/formalizing-fermats-last-theorem）。Claude agent 全自主完成，用了 11 天：1300 万行 Lean 代码——超过 Mathlib（人类积累至今的全部形式化数学库）的五倍体量——证明了 30,300 个定理，其中 29,500 个进入最终证明。总消耗约 60 亿输出 token，用的是一个 Anthropic 称"大致相当于 Fable 5.1"的内部研究模型。

感受一下这个时间线有多离谱：帝国理工的 Kevin Buzzard 是人类形式化费马大定理项目的领头人，他当年启动社区项目时的预期是"很多年"。FLT 是证明形式化领域的珠峰，底下压着几十年的现代数论。这次 Anthropic 和 Buzzard 合作，还联合了哥伦比亚大学做 Prove2Me 的团队——一个把工作组织成有向定理图的开放协作平台。Buzzard 的评价："如果 FLT 的自动形式化现在就能做到，那我们离整个现代数学文献的自动形式化近了一大步。"

全文最诚实的一个数字比标题更值钱：失败尝试占了非模板代码的约 7%。agent 们走了弯路、撞了死胡同、退回来重走——但最终收敛了，因为 Lean 是一个完美的验证器。1300 万行，每一行都要过一个不吃奉承的编译器，所以这个任何人类团队都无法手工核对的产物，反而是可信的。

这才是对数学之外所有做 agent 的人可迁移的教训：哪里有硬验证器，agent 的自主性就能放大到 11 天无人值守、60 亿 token；哪里没有，你得到的就是一个挤满 agent 互抄答案的德语 wiki。两个故事，同一周。