> 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 在丢番图《算术》书页空白处写下：当整数 
，不存在正整数 
满足 
。他还加了一句话：「我有一个真正绝妙的证明，但此处空白太小写不下。」
数学界今天普遍相信，那个「绝妙证明」如果存在，几乎肯定是错的——真正能证明这件事的技术，再过 358 年才被 Andrew Wiles 与 Richard Taylor 在 1994–1995 年造出来。129 页的论文横跨代数几何、数论、调和分析与交换代数，审稿期间还发现过一个关键漏洞，Wiles 与 Taylor 修补了整整一年。
Lean 形式化要做的事是把 Wiles 那 129 页的证明逐行翻成机器可核验的语言——人不读，一个极小的可信核（kernel）去查。
flowchart LR
A[Wiles 1995 证明
129 页自然语言] –> B[Lean 形式化
1300 万行代码]
B –> C[29500 中间定理
进入最终证明]
C –> D[Lean 核验证
仅 3 条公理]
style A fill:#1f2937,color:#fff
style B fill:#dbeafe,stroke:#2563eb
style D fill:#d1fae5,stroke:#059669
英帝国理工学院的 Kevin Buzzard 在 2024 年启动了一个 EPSRC 资助的五年社区项目，要把费马大定理形式化进 Lean，招募全球数学家参与，还发布了 86 页的形式化蓝图。整个社区的判断是这是数年级的工程。
Claude 11 天做完了。
🧰 为什么第一次尝试失败了，Prove2Me 又把它救了回来
项目并不是一上来就顺的。Anthropic 在研究帖里写得坦白：
– 早期使用标准 Claude Code 多 agent harness 失败了； – 失败原因不是模型不行——是架构不行：1300 万行代码、上万条中间定理，没有单个 agent 的上下文窗口能装下整个项目的状态； – 没有共享外部状态的多个 agent 会重复造轮子、互相覆盖工作，最后连「剩下要做什么」都说不清。
解法是 Prove2Me。这是 Tianyi Peng 在哥伦比亚大学的团队专门为长时间尺度 AI 形式化造的开源协作平台：
| 机制 | 解决的问题 |
|---|---|
| 定理 DAG | 每条定理是一个节点；定理之间的依赖是一条有向边 |
| 语句与证明分离 | Lean 编译时只重编译变更的文件，不必重编译整个项目 |
| 自然语言描述 | 每条定理有可搜索的 NL 描述，方便 agent 检索复用 |
| 多 agent 并行 | 新 agent 加入时先查 DAG：哪些已证、哪些在证、哪些待证 |
| 失败归档 | 死路不删，留给后续轮次使用 |
flowchart TD
A[Prove2Me 架构] –> B[定理 DAG]
A –> C[语句/证明分离]
A –> D[NL 描述]
A –> E[并行协作]
B –> B1[节点 = 定理]
B –> B2[边 = 依赖]
C –> C1[按文件切片编译]
C –> C2[避免重复编译]
D –> D1[可检索]
D –> D2[可复用]
E –> E1[几十个 agent
并行运行]
E –> E2[失败路径归档]
style A fill:#1f2937,color:#fff
style B1 fill:#d1fae5,stroke:#059669
在 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 陈述对齐。
flowchart LR
A[Claude Fermat 项目边界] –> B[做了什么]
A –> C[没做什么]
B –> B1[Wiles 证明
→ Lean 形式化]
B –> B2[29500 条中间定理]
B –> B3[Lean 三条公理
全核验证]
C –> C1[没有发现
新数学定理]
C –> C2[没有替代
人类数学家]
C –> C3[与 Mathlib 对齐
可整合]
style A fill:#1f2937,color:#fff
style B1 fill:#d1fae5,stroke:#059669
Kevin Buzzard 在评审后写道：
> 「Anthropic 研究员说只用了 11 天——这一非凡的形式化成就用除了数学公理之外没有任何假设证明了费马大定理。」
他更进一步：「如果 FLT 的自动形式化今天就能跑通，那么我们就朝现代数学文献的自动形式化迈出了重要一步。这些技术将带来新工具，在现有数学文库中找出错误，并减轻审稿人的负担。」
多伦多大学的数论学家 Daniel Litt 评价得更直接：「如果他们能形式化费马大定理，那么大概就能形式化任何东西。」
⚖️ 同周对比：Vinogradov 三素数定理，3 天、3 个消费者订阅
Anthropic 在同一研究帖里还披露了一个对照实验：
– 用 3 个 Claude Max 消费者订阅； – 在 Prove2Me 上跑 3 天； – 完成了 Vinogradov 三素数定理的形式化。
Vinogradov 定理说的是：每个充分大的奇数都能写成三个素数之和。它本身没有费马大定理那么久远、那么戏剧性，但它是解析数论里的核心结论之一。3 天搞定，说明大模型形式化这条管线已经在「消费者硬件 + 订阅」级别可负担。
flowchart TD
A[大模型自动形式化的
两个量级] –> B[11 天级别]
A –> C[3 天级别]
B –> B1[Fermat 大定理
Wiles 129 页
29500 中间定理]
C –> C1[Vinogradov
三素数定理
3 个 Max 订阅]
style A fill:#1f2937,color:#fff
style B1 fill:#fef3c7,stroke:#d97706
style C1 fill:#d1fae5,stroke:#059669
🧭 把这件事放进当周的 AI × 数学全景
当周还发生了至少三件同向的事：
| 项目 | 时间 | 关键数字 | 与 Fermat 项目的差异 |
|---|---|---|---|
| 字节跳动 Seed-Prover + 南开郭少明团队 | 9/9 | 三维粘性挂谷猜想形式化，180 万行 Lean，约 90% 由 Seed-Prover 完成 | 国内团队 / 不同子域 |
| FormaTheoria × 清华 + 丘成桐 | 9/1 | CFSG 4 个关键定理形式化到 99.4 万行 Lean | 群论子域 / 公开源代码 |
| OpenAI Astra Ten Proofs / Bel | 8 月 | 形式化 10 个数学结果 | 数学发现 + 形式化混合 |
| Google Antigravity Teamwork + Gemini 3.7 Flash | 9/1 | 解 7 个 FOCS/JMLR 开放问题（含 Knuth Cycles 猜想 40+ 页 Lean 验证） | 多智能体 + 不同工程栈 |
flowchart LR
A[2026 Q3
AI × 数学自动形式化] –> B[9/4 Anthropic Fermat]
A –> C[9/9 字节 Seed-Prover
挂谷猜想]
A –> D[9/1 FormaTheoria
CFSG 4 定理]
A –> E[8 月 OpenAI Astra
Ten Proofs]
A –> F[9/1 Antigravity
Knuth Cycles]
style A fill:#1f2937,color:#fff
style B fill:#d1fae5,stroke:#059669
style C fill:#fef3c7,stroke:#d97706
把这条线和当周的数学新闻放在一张图上，头部模型 + 形式化核验 + 公开 Lean 证书已经稳定地成为数学 AI 输出的一种标准形态。AI 不是在「发现」新数学，而是在把人类数学家写过的证明「搬」进一个机器可读、可核验的世界里。
🔁 这件事的意义：自动形式化从「论文里的承诺」变成「可重复的工程产出」
过去十年里，「自动定理证明 / 自动形式化」大多停留在 demo 级别——能跑能演示，但不能稳定交付一个能让数学家继续往上盖房子的工程产物。
这一波变化的核心是 Prove2Me 这类基础设施——把形式化任务切成一个 DAG，让几十个 agent 并行而不丢状态。基础设施补齐后，形式化的工作量瓶颈从「人」转到「算力 + 协调」，而 Claude Fable 5.1 / Max 订阅已经能把这笔算力成本压到社区项目级。
flowchart LR
A[自动形式化的瓶颈迁移] –> B[过去]
A –> C[现在]
B –> B1[依赖少数专家
+ 手工核验]
B –> B2[几年到十年]
C –> C1[几十个 agent + DAG]
C –> C2[天数级 /
订阅级]
style A fill:#1f2937,color:#fff
style C1 fill:#d1fae5,stroke:#059669
接下来值得追踪的几条线：
– 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