Anthropic 9/4 宣布完成费马大定理首个端到端经计算机验证的证明：在 Lean 中实现，只使用 Lean 的三个标准公理，走 Darmon–Diamond–Taylor 模性路线而非完整 Wiles 证明。这项工作在 11 天内「基本自主」完成：约 1300 万行 Lean 代码（超过 Mathlib 五倍）、29,500 个中间定理、约 60 亿输出 token；由哥伦比亚大学 Tianyi Peng 组的 Prove2Me 并行证明平台编排，运行在 Claude Code 多 agent 框架上，驱动模型为一个与 Claude Fable 5.1 大致相当的内部研究模型。另一个实验用三个 Claude Max 账户在 3 天内形式化了 Vinogradov 三素数定理。审查过这项工作的 Kevin Buzzard（Xena 项目）认可结果——Anthropic「抢先了他」。代码公开于 github.com/anthropics/fermats-last-theorem；HN 头条 442+ 分。
Anthropic 完成费马大定理的端到端形式化验证
2026-09-04前沿观察WATCH
Anthropic 9/4 宣布完成费马大定理首个端到端经计算机验证的证明：在 Lean 中实现，只使用 Lean 的三个标准公理，走 Darmon–Diamond–Taylor 模性路线而非完整 Wiles 证明。这项工作在 11 天内「基本自主」完成：约 1300 万行 Lean 代码（超过 Mathlib 五倍）、29,500 个中间定理、约 60 亿输出 token；由哥伦比亚大学 Tianyi Peng 组的 Prove2Me 并行证明平台编排，运行在 Claude Code 多 agent 框架上，驱动模型为一个与 Claude Fable 5.1 大致相当的内部研究模型。另一个实验用三个 Claude Max 账户在 3 天内形式化了 Vinogradov 三素数定理。审查过这项工作的 Kevin Buzzard（Xena 项目）认可结果——Anthropic「抢先了他」。代码公开于 github.com/anthropics/fermats-last-theorem；HN 头条 442+ 分。
本文来自既有扫描档案。迁移保留原判断，不代表在迁移时重新核验。
对你意味着什么
这是迄今最强的公开演示：agentic AI 加验证闭环可以完成搁置数十年的形式化任务——而且这套做法不止适用于数学：起草、跑检查器、把错误回灌、跨 agent 并行。任何做形式验证的团队（协议证明、kernel 不变式、规约一致性）今天就可以照搬这个编排模式，仓库就是参考实现。它也是本知识库趋势 #3 追踪的 multi-agent runtime 模式迄今最高调的真实工作负载。
前沿观察
公开材料与效果验证，分开看。
已记录的事实是工作及其材料已公开。论文或作者报告的效果不自动等于独立复现。下一步关注可复用代码、任务设置和第三方验证。
证据与关联材料
技术细节与六维评分
| 结果 | 费马大定理首个端到端经计算机验证的 Lean 证明；仅用 Lean 三个标准公理；走 Darmon–Diamond–Taylor 简化路线（非完整 Wiles 证明） |
|---|---|
| 规模 | 约 11 天基本自主完成；约 1300 万行 Lean（超 Mathlib 五倍）；29,500 个中间定理；约 60 亿输出 token |
| 技术栈 | Prove2Me 并行证明平台（哥伦比亚大学 Tianyi Peng 组）+ Claude Code 多 agent 框架；驱动模型为与 Claude Fable 5.1 大致相当的内部研究模型 |
| 第二实验 | 三个 Claude Max 账户 3 天形式化 Vinogradov 三素数定理 |
| 评审 | Kevin Buzzard（Xena 项目）审查并认可；称 Anthropic 抢先了他 |
| 代码 | github.com/anthropics/fermats-last-theorem |
| 反响 | HN 头条 442+ 分（9/4） |
技术影响 5
工程价值 3
采用信号 3
成熟度 3
验证成本 2
风险 1
历史更新原文
· Cross-link (2026-09-12 third-pass backfill): the Lean-verified AI-mathematics pattern repeated at Millennium scale within a week — OpenAI's Navier-Stokes solution (ev-20260908-18: ~10,000 agents, ~130B output tokens, Astra 17h Lean formalization) and the Alpoge-Buckmaster forced Euler resolution with an Anthropic internal model (ev-20260908-19); opened as trend #6 (AI-generated frontier mathematics).