9 月 4 日，Anthropic 宣布完成费马大定理的首个完整机器验证证明：Claude 在 11 天里以近乎自主的方式写出 1300 万行 Lean 代码，途中证明了 30,300 条定理，最终证明引用其中 29,500 条。整个证明只依赖 Lean 证明助手的三个标准公理，先后经过官方校验工具与一个独立 Rust 内核的全量检查。帝国理工学院的 Kevin Buzzard 编译了代码库并复核验证链，结论是证明成立。
这条定理还有另一层坐标意义：它是 Freek Wiedijk「100 个形式化挑战」清单的最后一项。这份运行了二十年的基准清单，就此收官。全部代码在 GitHub 仓库 anthropics/fermats-last-theorem 公开，Apache 2.0 许可。
从边页批注到 129 页论文
1637 年前后，费马在丢番图《算术》一书的边页写下：不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ（n 为大于 2 的整数），并称自己有一个页边写不下的绝妙证明。此后 350 多年，这个断言消耗了几代数学家。1908 年，德国设立 10 万金马克奖金征求证明，仅第一年就收到 621 份错误证明。1993 年 6 月，Andrew Wiles 在剑桥牛顿研究所用三天讲座宣布证明；两个月后，审稿人的一个提问暴露出关键漏洞，Wiles 与昔日学生 Richard Taylor 花了近一年修补，1995 年 5 月论文正式发表，全文 129 页。
机器验证的想法由荷兰计算机科学家 Jan Bergstra 在证明发表十年后提出：把数学推理改写成计算机能自动检查的形式。社区工程 2024 年才真正启动，Kevin Buzzard 发起多年度项目，目标是把 Wiles 的证明完整搬进 Lean，仅描述前期方案的 blueprint 文档就有 86 页。Anthropic 这次的结果把这条时间线推到了终点。
与 Anthropic 此前黎曼猜想相关研究（产出新数学结果）的定位不同，这次的新意在验证环节：像用计算器核对算式一样，核对一条 129 页的逻辑链。
证明走的路线：Frey 曲线到模性提升
Anthropic 团队选用的底本是 Darmon、Diamond、Taylor 三人 1995 年的技术性综述，它把 Wiles 与 Taylor 的原始论证整理成适合逐步展开的形态。数论界近年推进的现代证明（Khare、Taylor 等人的路线）不在这份仓库的范围内。
路线是现代数论的经典链条：费马方程若有一组反例解，就能构造出一条椭圆曲线（弗雷曲线）；Ribet 的水平下降定理证明，这条曲线的伽罗瓦表示不可能是模的，于是与谷山志村猜想矛盾；Langlands–Tunnell 定理给出模性论证的起点；Taylor–Wiles 补丁方法再把模性提升覆盖到整条曲线。官方发布的依赖图把全程分成三大模块：Mazur 关于艾森斯坦理想的工作、Ribet 定理、Wiles 的模性提升，最终汇入费马大定理本身。
人类数学家的介入被压缩到很少的几句方向性指令。项目发起人是 Anthropic 研究员 Tianyi Peng，他在哥伦比亚大学的团队研究方向就是 AI 形式化工具。全程指令的示例：「Jacobian as a scheme 听起来优先级很高」「尽快把 Mazur 定理推完」。
多智能体协作与两次尝试
最初的多智能体尝试以失败告终：智能体一度有进展，随后很快丢失项目全局状态，协作失效，这些失败的产物约占最终证明非样板代码行的 7%。第二次尝试切换到 Prove2Me，这是 Tianyi Peng 与哥伦比亚大学合作者设计的开放式数学形式化协作平台，把整条证明组织成可认领的定理依赖树：几十个 Claude 智能体在树上并行定义概念、证明中间定理，再用它们攻克更难的陈述，Lean 在每一步充当仲裁。
11 天消耗约 60 亿输出 token，底层模型是 Anthropic 一个内部通用研究模型，官方描述其能力与 Claude Fable 5.1 大致相当。8 月 18 日 02:00:57（UTC），依赖树根节点翻成 PROVED，智能体日志里写着「FLT root reads PROVED ... This is the campaign's goal」。
60 亿 token 折成钱是多少？Buzzard 博文评论区里 David Jao 按 API 牌价算出约 30 万美元。Buzzard 本人的对照更直接：他拿英国工程和物理科学研究理事会（EPSRC）的 100 万英镑经费跑五年项目，Anthropic 只用了 11 天，他同时怀疑对方实际花费远高于此。
三道互相独立的机器验证
这次结果的可信度建立在三道可复现的检查上，仓库 README 把每一道的成本写到了小数点。
第一道是完整构建。lake build 从源码编译 Mathlib 与全部 60,475 个模块（Lean 4.33.1，含 2026 年的内核健全性修复），每个声明都经 Lean 内核检查。所有模块不含 sorry、自定义 axiom、native_decide、unsafe、extern、implemented_by、partial def、#eval 中的任何一项。FinalCheck.lean 用 #print axioms 断言主定理只依赖 propext、Classical.choice、Quot.sound 三个标准公理，多一个公理构建直接失败。
第二道是陈述对齐。leanprover/comparator 工具检查被证陈述与 Mathlib 官方的费马大定理陈述逐常量一致，再把整个证明连同 Mathlib 在内核里重放一遍，输出结论「Your solution is okay!」。
第三道是独立内核。nanoda 0.4.13 用 Rust 实现了另一套 Lean 内核，对 37.8 GB 的环境导出做全量检查，1,052,234 个声明零错误。仓库为它打上的四个补丁只增加进度输出与定义等价搜索的加速，不改任何类型规则。
| 检查 | 工具 | 耗时 | 峰值内存 |
|---|---|---|---|
| 全量构建 | lake build（96 核） | 5 小时 32 分 | 153 GB |
| 陈述对齐 + 内核重放 | comparator v4.33.0 | 约 15 小时 | 230 GB |
| 独立内核全量检查 | nanoda 0.4.13（Rust） | 约 30 分钟（16 线程） | 40 GB |
磁盘同样是门槛：构建产生约 67 GB 的 .lake/ 目录与约 220 GB 的 C 文件，comparator 重放官方建议预留 300 GB 内存。
Buzzard 的核对与两段评价
证明发布当天，Kevin Buzzard 编译了代码库、运行 comparator，「它通过了」。他实测的体量：超过 1340 万行（Anthropic 博客表述为 1300 万行），是 Mathlib 数学库的 5 倍以上，编译耗时接近 Mathlib 全库的 20 倍，在 96 核机器上完成；在 Anthropic 提供的 500 GB 内存机器上，跨文件跳转仍会让 Lean 明显卡顿。
他对这项工作的定性分成两层。数学层面：「这项工作基本什么也没告诉我们。」他自己对 Wiles 证明正确性的把握是 99.9%，数论学界多数人是 100%，这次形式化忠实跟随了早期文献，没有添加新数学。能力层面：「它告诉我们的是这个领域里什么已经成为可能。」几千页文献可以由 AI 集群在 11 天内端到端形式化，意味着现代研究的形式化会开始与研究同步发生；机器会逐条检查朗兰兹纲领里的论证，标记其中不完整的环节；论文评审负担会下降；那些依赖「专家都知道」假设的论文会被精确暴露。
Buzzard 自己的 EPSRC 项目没有被替代。他承诺的交付包括向 Mathlib 提交现代数论基础对象的 PR（进行中），以及一份让人类读者逐层探索现代证明（Khare、Taylor 等人路线）的动态文档。他判断 Anthropic 不会做第二件事，因为对方形式化的本来就不是现代证明。
与这个定理的两次擦肩，被他写成了一段自嘲。1993 年他还是二年级研究生，听了 Wiles 第一场讲座觉得完全看不懂，翘掉后两场去了爱尔兰度假，一周后回剑桥才听说费马大定理被证明。2026 年 8 月收到 Anthropic 标题为「End-to-end Lean formalization of Fermat's Last Theorem」的邮件时，他在威尔士 Green Man 音乐节，手机信号差，把发件人当成了民科，一周后清理近千封未读邮件时才知道发生了什么。
代码库：为机器检查而写
这份代码不为阅读而生。命名由机器生成，P2M 与十六进制后缀是流水线标签而非数学记号；注释除上游声明与引用记录外全部移除；README 建议读者以陈述本身为准判断每个定理的含义。Anthropic 在脚注里承认：Mathlib 简洁且经充分评审，这份证明「很可能比必要的长度长得多」。
指数覆盖上，Buzzard 核对了拼图：这份仓库与 flt-regular 项目（Best、Birkbeck、Brasca、Rodriguez 此前完成的奇正则素数情形）各覆盖一部分，最小的非正则素数是 37，两者拼接后指数覆盖完整。仓库的出处声明同样清楚：106 个文件衍生自帝国理工学院的 FLT 项目，23 个文件复用或重证 Mathlib 引理，逐文件列在 ATTRIBUTION.md。
为人类读者准备的入口是仓库里约 390 MB 的 html 目录：29,511 个定理页、1,450 个定义模块、全文搜索与依赖图，离线可用。README 第一行写着：研究产物，不维护，不接受贡献。
订阅级别的后续实验
Anthropic 在文末给了一个量级参照：三个个人 Claude Max 订阅通过 Prove2Me 协作，3 天完成维诺格拉多夫三素数定理的形式化。Buzzard 预期的工作方式随之改变：论文附带机器可查的证明成为常态，形式化不替代面向人的阐述，但可能是数学界跟上 AI 产出速度的唯一可行途径。
仓库与验证脚本都已公开。一台有 300 GB 内存的机器加上约一天时间，就能完整重放这个 350 多年问题的机器验证。