Anthropic 9 月 4 日发文，说 Claude 用 11 天基本自主地完成了费马大定理的形式化证明，写在 Lean 里，全程可由计算机检查。
数字给得很足。1300 万行 Lean 代码，是社区主库 Mathlib 的五倍多。产出 30300 条经计算机验证的定理，其中 29500 条用在最终证明里。消耗约 60 亿输出 token，跑的是一个内部通用研究模型，Anthropic 说它大致相当于 Claude Fable 5.1。最终证明只用到 Lean 的三条标准公理，另有比对工具确认命题和 Mathlib 里那版费马大定理一致。早期几次失败的尝试也没白跑，最终证明里约 7% 的非样板代码来自那些挂掉的运行。
审稿的是帝国理工的 Kevin Buzzard，他从 2024 年起带着社区做同一件事。他的评价是这是一项非凡的自动形式化成就，在数学公理之外没有任何额外假设。
Anthropic 自己把边界划得很清楚。这不是新数学，Claude 走的是 Darmon、Diamond 和 Taylor 那版简化证明，没有另想一条路。文章拿它和 Anthropic 之前的黎曼猜想工作对照，那次产出的是新数学，这次新的地方在验证。过程也不是完全无人干预，研究者 Tianyi Peng 时不时给一点优先级方向上的提示，而且换到 Prove2Me 平台之后才跑通。
文章的脚注里还有一句，作者说这份证明大概比它需要的长得多。去掉生成的样板还剩约 1050 万行，目前也不是能并进 Mathlib 的形态。同一次实验里还有个副产品，维诺格拉多夫三素数定理的形式化花了 3 天。