Anthropic 完成费马大定理的端到端形式化验证

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 模式迄今最高调的真实工作负载。