2026 年 9 月 4 日，Anthropic 公开了费马大定理的完整形式化证明，可由 Lean 4 证明助手逐步检查。数十个 Claude Agent 在 11 天内生成约 1300 万行 Lean，累计完成 30300 个可机检定理，其中约 29500 个进入最终证明。公司披露，这次运行消耗约 60 亿输出 token，所用的是一款能力大致相当于 Claude Fable 5.1 的通用内部研究模型。
Andrew Wiles 与 Richard Taylor 在 1990 年代已经完成费马大定理的数学证明。Claude 沿用的主要是 Darmon、Diamond 与 Taylor 在 1995 年阐释的既有路线，将其中的定义和推导转为 Lean 能逐步检查的代码。此次进展在于，AI 以较大规模完成了这种转换，并让完整证明通过机器核验；它并未找到新的数学证明路线。
数十个 Agent 如何分工完成证明
Anthropic 的早期尝试并不顺利。官方复盘称，Agent 虽然能局部推进，却很快丢失项目状态，停止有效协作；这些失败尝试仍占最终非样板代码约 7%。团队随后引入 Prove2Me 平台，并用建立在 Claude Code 之上的多 Agent 运行框架协调工作。
Prove2Me 用有向无环图记录各个定理的依赖关系，让 Agent 知道哪些结论需要先证明。每个定理的“陈述”和“证明”被拆成独立对象：陈述固定、环境版本锁定，一份陈述可以接受不同 Agent 提交的证明。Agent 先写出证明思路，再把大定理逐层拆成可以独立解决的子定理。最底层的子定理在对应 Lean 环境中编译通过后，上层证明就能调用这些结果，继续推进。
这个设计同时解决了三类工程问题。第一，依赖图和经过人工审核的阶段目标，让 Agent 知道接下来处理哪项任务，减少长时间工作后遗漏进度的问题；第二，陈述与证明分离，减少一次证明修改触发整个下游重新编译的成本；第三，每个定理附带自然语言说明并进入可搜索库，Agent 被要求先搜索、再复用，减少不同 Agent 重复证明相同结论的情况。
因此，完成这项工作需要的不只是增加 Agent 数量。早期尝试中出现的协作问题，需要靠明确的任务关系、固定的定理陈述、编译检查和共享检索一起解决。人类也没有完全退出：Anthropic 研究员 Tianyi Peng 曾给出“优先处理 Jacobian”“尽快推进 Mazur 定理”等高层指令。在这次运行中，Agent 承担了大量具体任务，人类仍会不时调整工作重点。
机器核验通过后，中间定理仍需人工审阅
公开仓库把“机器核验”分成了三道检查。第一，默认构建目标在 Lean 4.33.1、Mathlib v4.33.0 上从源码编译 60475 个模块；最终定理只能依赖 Lean 的三个标准公理 propext、Classical.choice 与 Quot.sound，不能留下 sorry、新增 axiom 或 native_decide 等绕过路径。
第二，comparator 使用一份只导入 Mathlib 的挑战文件，逐项核对最终费马大定理陈述及其涉及的常量是否与标准环境一致，并用 Lean 内核重新检查整条证明依赖链。这一步防止系统证明了一个名称相似、实际更弱或偷偷改过定义的命题。第三，独立的 Rust 内核 nanoda 接受了同一环境导出的 1052234 个声明，为单一内核实现之外再加一层交叉检查。
Imperial College London 形式化项目负责人 Kevin Buzzard 表示，他已编译整套代码并运行 comparator，结果通过。仓库给出的最终定理也确实是普通自然数上的标准表述：当指数 n ≥ 3，不存在正自然数 a、b、c 使 aⁿ + bⁿ = cⁿ。
但 Lean 检查的是“某个项是否具有某个类型”，不会判断中间定理的英文名称是否忠实概括其数学意义。仓库自己也把这一层留给读者，并用 PROOF-PATH.md 映射经典步骤与对应的 Lean 定理。最终命题经过 comparator 锁定，足以支持“费马大定理已端到端机器核验”；它不等于 1300 万行代码已经获得逐段的人类数学审阅。
11 天的运行与五年社区项目，目标和起点不同
最显眼的比较基线是 Imperial College London 自 2024 年启动、计划延续到 2029 年的社区项目。但两者目标和路线并不相同。Imperial 选择吸收 Khare–Wintenberger、Kisin 等后续工作的现代路线，并计划把可复用的现代数论基础持续提交到 Mathlib；Anthropic 则选择更接近 Wiles–Taylor-Wiles 原证明的 Darmon–Diamond–Taylor 路线，以尽快完成最终命题的证明。
Anthropic 的产物也不是从空白开始。仓库归属文件列出 106 个包含 Imperial FLT 或 flt-regular 项目材料的 Lean 文件，另有 23 个文件复现或改写了 Mathlib 文本。完整证明对指数 5 使用自包含下降法，对 7、11、13 等情形复用了 flt-regular 已形式化的规则素数路线，再把主要工程量放在更大素数所需的 Mazur、模性提升和降层等链条上。
这些复用说明，已有形式化数学成果为此次工作提供了基础。因此，“11 天”与“五年”无法直接换算成效率倍数：两个项目的证明路线、可用代码库、目标产物和维护方式均不同。
1300 万行代码的长期维护仍待解决
Anthropic 称这份证明的行数超过 Mathlib 五倍，同时在脚注中承认 Mathlib 更精炼、经过更充分审阅，当前产物可能远长于必要长度。公开仓库进一步标注其为“不维护、不接受贡献”的研究制品。仓库提供了离线 HTML、定理依赖图和搜索入口，方便读者浏览。至于如何精简和重构这些生成代码、把可复用的部分纳入公共库，目前仍没有解决。
复现门槛也很高。仓库记录的从零构建在 96 个并行任务下耗时 5 小时 32 分，峰值内存 153GB；comparator 约需 14 小时 46 分、峰值内存 230GB。60 亿输出 token 也无法直接换算成可复制的项目成本，因为内部模型、推理价格、失败重试和编译资源均未完整披露。
接下来值得关注的是，这些生成代码能否经过整理，进入 Mathlib 这类持续维护的数学库。具体问题包括：能否合并重复定理、减少需要逐一审阅的内容；依赖库接口变化后，能否以较低成本适配；其他团队使用公开模型和算力，能否复现同一运行框架的结果。完整证明已通过机器核验，如何让它便于阅读、复用和维护，仍是一项长期工作。
