Claude 用 11 天把费马大定理「搬」进 Lean：1300 万行代码、29500 条定理，Anthropic 用多智能体啃下了 350 年悬案的形式化

2026 年 9 月 4 日，Anthropic 宣布 Claude 在 11 天内完成了费马大定理的首次端到端、计算机可逐步验证的 Lean 形式化证明。整个项目写了约 1300 万行 Lean 代码，证明约 30300 条定理，其中 29500 条进入最终证明，消耗约 60 亿输出 token。证明路线沿着 Darmon–Diamond–Taylor 对 Wiles 1995 年证明的简化版展开，Lean 仅凭三条标准公理完成验证。项目由 Anthropic 研究员 Tianyi Peng 领衔，使用他和哥伦比亚大学团队开发的开源平台 Prove2Me——它把定理记成有向无环图（DAG），让几十个 Claude agent 并行工作而不丢项目状态。同一周，三个消费者级 Claude Max 订阅用 3 天完成了 Vinogradov 三素数定理的形式化。

📜 三百五十年的命题，11 天的形式化

1637 年，法国数学家 Pierre de Fermat 在丢番图《算术》书页空白处写下：当整数 \(n > 2\)，不存在正整数 \(a, b, c\) 满足 \(a^n + b^n = c^n\)。他还加了一句话：「我有一个真正绝妙的证明，但此处空白太小写不下。」

数学界今天普遍相信，那个「绝妙证明」如果存在，几乎肯定是错的——真正能证明这件事的技术，再过 358 年才被 Andrew Wiles 与 Richard Taylor 在 1994–1995 年造出来。129 页的论文横跨代数几何、数论、调和分析与交换代数，审稿期间还发现过一个关键漏洞，Wiles 与 Taylor 修补了整整一年。

Lean 形式化要做的事是把 Wiles 那 129 页的证明逐行翻成机器可核验的语言——人不读，一个极小的可信核（kernel）去查。

英帝国理工学院的 Kevin Buzzard 在 2024 年启动了一个 EPSRC 资助的五年社区项目，要把费马大定理形式化进 Lean，招募全球数学家参与，还发布了 86 页的形式化蓝图。整个社区的判断是这是数年级的工程。

Claude 11 天做完了。

🧰 为什么第一次尝试失败了，Prove2Me 又把它救了回来

项目并不是一上来就顺的。Anthropic 在研究帖里写得坦白：

• 早期使用标准 Claude Code 多 agent harness 失败了；
• 失败原因不是模型不行——是架构不行：1300 万行代码、上万条中间定理，没有单个 agent 的上下文窗口能装下整个项目的状态；
• 没有共享外部状态的多个 agent 会重复造轮子、互相覆盖工作，最后连「剩下要做什么」都说不清。

解法是 Prove2Me。这是 Tianyi Peng 在哥伦比亚大学的团队专门为长时间尺度 AI 形式化造的开源协作平台：

在 Prove2Me 上跑出来的成绩有几个数字值得记：

• wall-clock 11 天（不是单 agent 连续 11 天，是几十个 agent 并行跑的日历时长）；
• 约 60 亿输出 token，模型大致对标 Claude Fable 5.1；
• 失败早期尝试贡献了最终证明非 boilerplate 代码约 7%——它们并非完全浪费；
• Lean 验证后生成的最终证明是 Mathlib 的 5 倍以上。

📐 它证了什么，没证什么

需要把这条线精确地划清楚：

• 它没证「Claude 自己发现了费马大定理的证明」。那是 Wiles 1995 年做的事。
• 它证的是：Wiles 的人类证明可以被自动翻译成机器可逐步验证的 Lean 形式。
• 证明路线沿用了 Darmon–Diamond–Taylor 对 Wiles 证明的简化重述。
• Lean 用自身三条标准公理完成验证，没有额外假设。
• 一名 comparator 确认定理陈述与 Mathlib 自家 FLT 陈述对齐。

Kevin Buzzard 在评审后写道：

「Anthropic 研究员说只用了 11 天——这一非凡的形式化成就用除了数学公理之外没有任何假设证明了费马大定理。」

他更进一步：「如果 FLT 的自动形式化今天就能跑通，那么我们就朝现代数学文献的自动形式化迈出了重要一步。这些技术将带来新工具，在现有数学文库中找出错误，并减轻审稿人的负担。」

多伦多大学的数论学家 Daniel Litt 评价得更直接：「如果他们能形式化费马大定理，那么大概就能形式化任何东西。」

⚖️ 同周对比：Vinogradov 三素数定理，3 天、3 个消费者订阅

Anthropic 在同一研究帖里还披露了一个对照实验：

• 用 3 个 Claude Max 消费者订阅；
• 在 Prove2Me 上跑 3 天；
• 完成了 Vinogradov 三素数定理的形式化。

Vinogradov 定理说的是：每个充分大的奇数都能写成三个素数之和。它本身没有费马大定理那么久远、那么戏剧性，但它是解析数论里的核心结论之一。3 天搞定，说明大模型形式化这条管线已经在「消费者硬件 + 订阅」级别可负担。

🧭 把这件事放进当周的 AI × 数学全景

当周还发生了至少三件同向的事：

把这条线和当周的数学新闻放在一张图上，头部模型 + 形式化核验 + 公开 Lean 证书已经稳定地成为数学 AI 输出的一种标准形态。AI 不是在「发现」新数学，而是在把人类数学家写过的证明「搬」进一个机器可读、可核验的世界里。

🔁 这件事的意义：自动形式化从「论文里的承诺」变成「可重复的工程产出」

过去十年里，「自动定理证明 / 自动形式化」大多停留在 demo 级别——能跑能演示，但不能稳定交付一个能让数学家继续往上盖房子的工程产物。

这一波变化的核心是 Prove2Me 这类基础设施——把形式化任务切成一个 DAG，让几十个 agent 并行而不丢状态。基础设施补齐后，形式化的工作量瓶颈从「人」转到「算力 + 协调」，而 Claude Fable 5.1 / Max 订阅已经能把这笔算力成本压到社区项目级。

接下来值得追踪的几条线：

• Mathlib 整合：Claude 生成的 1300 万行 Lean 里有约 29500 条中间定理，把其中一部分并入 Mathlib 仍需要 Buzzard 团队大量手工工作；
• 领域扩张：自动形式化能否同样推到偏微分方程、流形学习、量子场论等机器辅助之前更少触达的子域；
• 审稿流程：AI 生成的证明能否在未事先声明的情况下进入人类审稿流水线，「机器可信 + 人可信」 双层背书的协议正在被重新设计；
• 错误扫描：Buzzard 提到的「在现有数学文库中找错」——自动形式化未来也许会反向输出**「哪些被广泛引用的结论其实有未声明的假设」**。

📚 参考文献

1. Nature News：Anthropic AI 'formalizes' proof of Fermat's last theorem in just 11 days，2026-09-07（doi: 10.1038/d41586-026-02822-9）
2. Anthropic Research Post：First complete computer-checked proof of Fermat's Last Theorem，2026-09-04
3. Tech Times：Fermat's Last Theorem Machine-Checked — Claude Completes in 11 Days，2026-09-05
4. AI Base：Mathematical Milestone in the AI World — Claude Achieves End-to-End Formalization，2026-09-04
5. AI Weekly：Claude formalized Fermat's Last Theorem in 11 days，2026-09
6. 光明网 / 今日头条：AI 首次「形式化」证明费马大定理，2026-09-09
7. Kevin Buzzard 在 Anthropic 研究帖下的官方评审陈述
8. 南开大学：三维粘性挂谷猜想形式化验证（与字节跳动 Seed-Prover 合作），2026-09-09

#FermatLastTheorem #Lean #自动形式化 #Claude #Anthropic #Prove2Me #数学AI