AREX Feed Article
Nature 报道 Anthropic 宣称：Claude 11 天形式化验证费马大定理，写下约 1,300 万行代码
科学期刊 称，总部位于旧金山的 Anthropic 宣称，其 Claude 模型已「形式化验证」了 Andrew Wiles 与 Richard Taylor 的费马大定理证明。模型用 11 天写下约 1,300 万行 Lean 代码，可由计算机逐行核验；Nature 报道称，这个项目原本预计要耗费人类约 10 年。
，把核心信息概括为：Anthropic「形式化」了 Wiles 与 Taylor 的费马大定理证明。Nature 的文章称，这是这一著名猜想首次被改写成计算机核验的代码。
需要先说明口径：上述规模数字与「已完成」的结论都出自 ，Nature 的报道是对公告的转述与对数学家的访谈，公告本身只能证明公司作出了这一声明。
Andrew Wiles 站在普林斯顿大学办公室里，身后黑板写着他证明的费马大定理。图片来源：AP Photo/Charles Rex Arbogast/Alamy，为 Nature 报道配图。
形式化：把证明的每一步都写给机器看
所谓形式化（formalization），是把数学家用自然语言写成的论证，逐句翻译成证明助手 Lean 能够自动检查的代码。人写的证明会省略显而易见的步骤，Lean 要求每一步都显式出现，因此代码体量远超原论文。
Anthropic 公告给出的账目是：Claude 沿途证明了 30,300 个中间定理，其中 29,500 个进入最终证明；整个代码库超过 Lean 社区主数学库 Mathlib 体量的 5 倍，是迄今最大的 Lean 证明。公司称，完成的证明由 Lean 检查通过，只依赖 Lean 的三条标准公理，另有对照程序确认，定理陈述与 Mathlib 中费马大定理的陈述一致。
Anthropic 方面表示，Claude 的版本遵循 Henri Darmon、Fred Diamond 与 Richard Taylor 对 Wiles 证明的简化阐述。
129 页的证明，为什么还要机器再查一遍
费马大定理断言，不存在正整数 x、y、z，使等式 xⁿ + yⁿ = zⁿ 在 n 大于 2 时成立。1637 年，Pierre de Fermat 在《算术》一书页边写下这一断言，附了一句流传至今的话：「我发现了对此一个真正奇妙的证明，可惜这儿的空白太窄，写不下。」
此后 350 多年无人给出证明。Anthropic 的公告回顾称，1908 年有人悬赏 10 万德国金马克（约合今天的 100 万～200 万美元），仅第一年就收到 621 个错误尝试。
1993 年 6 月，Wiles 用三天系列讲座宣布证明完成。核查进行到约两个月时，一位审阅者的提问暴露了关键缺口；Wiles 先独自、后与昔日学生 Richard Taylor 合作修补了近一年，一度濒临放弃，最终靠一个早先搁置的思路补上漏洞。修正后的证明于 1995 年 5 月发表，正文 129 页，Wiles 也因此在 2016 年获得阿贝尔奖。
Anthropic 在公告里用这段历史说明人类验证之难：数学家反复检查数月，缺口仍能潜伏其中。把 Wiles 证明形式化的提议可追溯到 2005 年，荷兰计算机科学家 Jan Bergstra 当年提出这一方向；2024 年，帝国理工学院数学家 Kevin Buzzard 又发起多年期的社区形式化项目，仅项目蓝图就写了 86 页；Anthropic 公告称，整个形式化工作原本预计需要数年。
今年 2 月，AI 已核验过菲尔兹奖得主 Maryna Viazovska 关于 8 维与 24 维球最密堆积的证明。
60 亿 token、数十个智能体：一次「大体自主」的协作
这次工程被 Anthropic 公告描述为「大体自主」的协作。测试由 Anthropic 研究员 Tianyi Peng 发起，他的团队在哥伦比亚大学开发 AI 形式化工具；这次干活的是 Anthropic 的内部研究模型，公告称其能力「大致相当于 Claude Fable 5.1」。
项目开局并不顺利：多个 Claude 智能体很快丢失项目状态、协作失效，这些失败尝试的产出仍占最终代码非样板行的约 7%。转折点是换用 Prove2Me，这是 Peng 与哥伦比亚大学合作者设计的开源形式化协作平台。
Prove2Me 用一张有向无环图维护定理间的依赖关系，让智能体决定下一步该证明什么；把定理陈述与证明分文件存放，加速 Lean 编译；还为每条定理保留自然语言描述，便于搜索复用。在此基础上，基于 Claude Code 的多智能体框架开始工作：数十个智能体分工定义概念、证明中间定理、逐层逼近更难的结论，人类只给出少量高层指令，例如「把 Mazur 定理往前赶」。
Anthropic 公告配图：Prove2Me 计划的关键里程碑图。三个色块分别对应 Claude 必须证明的三个核心子定理（Mazur 的表示不可约性、Ribet 的降阶、Wiles 的半稳定模性），最底部的橙色框即最终目标费马大定理。
Anthropic 贴出的 Claude 工作日志显示，2026 年 8 月 18 日 02:00:57（UTC），证明根节点在 Prove2Me 上显示「PROVED」。整个工程消耗约 60 亿个输出 token，从开工到完成用了 11 天。
「彻底震撼了我」，但「基本没告诉我们新东西」
Nature 的报道引述了三位数论学家的评价。罗格斯大学数论学家 Alex Kontorovich 的评语是：一台机器能把人类数学家的工作变成 1,300 万行之长、无懈可击的证明，「彻底震撼了我」。多伦多大学数论学家 Daniel Litt 的判断是：「如果他们能形式化费马大定理，他们大概能形式化一切。」Buzzard 则给出参照系：与今年 2 月被 AI 核验的球堆积证明相比，费马大定理「也许要难一个数量级」。
Buzzard 的处境特殊：被 Anthropic 请来审阅这份证明的人，自己正主持着英国 EPSRC 资助的费马大定理形式化项目（100 万英镑、5 年期）。Anthropic 的成果还吸收了他领导的帝国理工项目与 flt-regular 项目的代码。
他在里记录，自己编译了整个代码库并运行对照程序，「检查通过」；代码量超过 1,340 万行，编译耗时约为 Mathlib 的 20 倍。他最初甚至把 Anthropic 的审阅邮件当成骗子来信，当时他正在威尔士的音乐节上，一周后才在近 1,000 封未读邮件里发现真相。
但 Buzzard 也直接说，这项工作在数学上「基本没有告诉我们新东西」；他本人对费马大定理成立有 99.9% 的把握，数论学界多数人是 100%。他还指出，Anthropic 形式化的是 Darmon–Diamond–Taylor 的 1995 年阐述，并非他自己正在做的、基于 Khare–Taylor 等后续工作的「现代证明」；其真正价值在于自动形式化能力本身，也补上了 Freek Wiedijk 百道形式化挑战清单的最后一道，为这项 20 年的基准画上句号。
他半开玩笑地算了一笔账：「Anthropic 只花了 11 天，不过我倒想知道他们花了多少钱。」博客评论区里，署名 David Jao 的读者按 API 价格估算，60 亿个输出 token 约合 30 万美元。
从复核这份证明，到审查整座知识库
Anthropic 公告称，全部代码已发布在 GitHub 上，并附有文字导览。
Nature 报道认为，这一结果显示，AI 在检查数学家的工作方面将扮演越来越重要的角色，也会参与产出新的数学推理。Anthropic 的判断更具体：评估一个新结果可能要花数月乃至数年，若能随手附上机器核验的证明，人类审稿的负担就会减轻；公司预期，形式化证明与给人读的阐述并行将成为常态。
Anthropic 研究人员用三个个人版 Claude Max 订阅做过一次小实验，全程通过 Prove2Me 协作，3 天完成了维诺格拉多夫三素数定理的形式化。Anthropic 还宣布与其它实验室一起扩大对外部研究者的免费与折扣订阅支持，并设专项资助，用于形式化其它大定理或改进 Lean 与 Mathlib。
Buzzard 在 Nature 报道里给出了更远的判断：按目前的进展速度，AI 或许很快就能审查整座数学知识库，甚至发现某些著名结果是错的。「两年前，这还是幻想。」