Claude 用 11 天完成费马大定理形式化，1300 万行 Lean 代码通过机器验证

Anthropic 于 2026 年 9 月 4 日公布，费马大定理已经有了一份可由计算机全程验证的证明。绝大部分工作由 Claude 完成，历时约 11 天，写出的 Lean 代码达到 1300 万行，最终证明中用到了 29500 条中间定理。这并没有诞生新的数学成果，但验证证明这件事的速度，已经和过去完全不在一个量级上。

走了 350 年的证明，和它背后的验证难题

费马把那句话写在书页空白处，大约是 1637 年。对任意大于 2 的指数，不存在正整数 a、b、c 满足 a 的 n 次方加 b 的 n 次方等于 c 的 n 次方。命题本身谁都读得懂，证明却 350 多年无人给出。1908 年有人悬赏 10 万金马克，仅第一年就收到 621 份错误证明。※该奖金按今天的币值约合 100 万至 200 万美元（约 1.6 亿至 3.1 亿日元）。按 1 美元 = 156 日元换算。

真正了结此事的是 1995 年 Andrew Wiles 那篇 129 页的论文。这份证明同样没有被立刻接受。1993 年演讲中公布的初版在审查过程中被指出存在关键漏洞，Wiles 花了一年时间，和昔日学生 Richard Taylor 一起把缺口补上。而要读通这 129 页并确认无误，多位数学家投入了数月时间。

形式化的思路正是从这里来的：把证明改写成机器能读的语言，让计算机去找逻辑漏洞。写给人看的证明会把大量步骤视为显然而跳过，而证明助手 Lean 要求每一步都写清楚。就费马大定理而言，Imperial College London 的 Kevin Buzzard 于 2024 年发起的社区项目一直在推进，仅描述初始阶段的设计蓝图就有 86 页。这原本被认为是以年为单位的工程。

11 天，1300 万行

推动这件事的是 Anthropic 研究员 Tianyi Peng。他在 Columbia University 的团队一直在做形式化工具，他想试试 Claude 能在这个难题上走多远，结果超出了预期。

数字能说明规模。11 天生成 1300 万行 Lean 代码，途中证明了 30300 条定理，其中 29500 条进入最终证明。作为依托的 Mathlib 是社区最核心的数学证明库，而这份证明的体量是它的 5 倍以上。Anthropic 自己也承认，写法很可能比实际需要的冗长得多。

证明路线并非 Wiles 的原始论证，而是以 Henri Darmon、Fred Diamond 和 Richard Taylor 的简化讲解为底本。人类的介入仅限于偶尔给出的高层建议，例如把作为概形的雅可比优先处理。最终证明只依赖 Lean 的三条标准公理，并通过专门的比对工具确认了所证命题与 Mathlib 中费马大定理的表述一致。

这份成果并非凭空而来。它从 Buzzard 的项目以及处理正则素数情形的 flt-regular 中吸收了组件，而 Lean 与 Mathlib 本身就是数百位数学家共同养成的产物。Buzzard 在读过这份证明后指出，AI 自动形式化的产物如今已经稳固到可以被别人拿来继续搭建的程度。