Anthropic 于 2026 年 9 月 4 日公布了一项大规模数学形式化工作：Claude 在 Lean 4 中完成了费马大定理的端到端机器可检查证明。这里的成果不是发现一条新的数学证明路线，而是把已有的 Wiles、Taylor–Wiles 等人的论证转换成证明助手能够逐步核验的形式。
英文原文与中文翻译
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.
Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of the most famous theorems of all time. This was a project experts thought would take many years. It is the largest Lean proof ever written.
Fermat’s Last Theorem was first proven in 1995 by Sir Andrew Wiles, more than 350 years after it was conjectured. Our proof, which totals over 13 million lines of code, provides machine verification. More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized.
We see this as a major step in the long process of firming up the core of mathematical knowledge, building on work from three centuries of mathematicians and hundreds of contributors to Lean and Mathlib.
We are optimistic that AI-assisted verification of mathematical proofs will help reduce the burden of refereeing mathematics in an era where more proofs are being produced than ever before.
You can read about the process on our Science Blog: Formalizing Fermat's Last Theorem \ Anthropic
And see the complete proof on GitHub: GitHub - anthropics/fermats-last-theorem · GitHub
检查一个重要数学证明是否正确可能需要数年时间。形式化——把数学推理转换为 Lean 等计算机证明助手可以核验的形式——能够提供帮助。
上个月，Claude 完成了费马大定理的首个形式化证明。费马大定理是史上最著名的定理之一，而专家此前认为这个形式化项目可能需要很多年。这也是迄今规模最大的 Lean 证明。
费马大定理由安德鲁·怀尔斯爵士于 1995 年首次证明，距离它被提出已有 350 多年。Anthropic 的形式化证明包含超过 1300 万行代码，提供了机器核验；更重要的是，它还证明了最终证明所需的 29000 多个其他定理，涉及多个此前从未形式化的数学领域。
Anthropic 将其视为巩固数学知识基础这一长期进程中的重要一步。该成果建立在三百年来数学家的工作，以及数百名 Lean 和 Mathlib 贡献者的成果之上。
Anthropic 认为，在证明产量不断增加的时代，AI 辅助的数学证明核验有望减轻数学同行评审的负担。
完整过程见 Anthropic Science Blog，完整证明见公开 GitHub 仓库。
实际完成了什么
Anthropic 的技术说明称，Claude 在 11 天内、以较高自主程度完成了端到端形式化。数十个 Claude 智能体协作定义概念、证明中间定理并复用已有结果，共消耗约 60 亿个输出 token；使用的是能力大致可比 Claude Fable 5.1 的内部通用研究模型。
最终工程包含约 1300 万行 Lean 代码。过程中生成约 30300 个可由计算机核验的定理，其中约 29500 个进入最终证明。证明遵循 Frey、Serre、Ribet、Wiles 和 Taylor–Wiles 的路线，主要依据 Darmon、Diamond 与 Taylor 的简化阐释。
这项工作的关键并不只是模型本身，还包括 Prove2Me 协作系统和基于 Claude Code 的多智能体执行框架。Prove2Me 提供了三个重要机制：
- 用有向无环图维护定理陈述和依赖关系，让多个智能体知道下一步应处理哪个证明；
- 将定理陈述与证明拆分到不同文件，缩短 Lean 编译时间并降低资源消耗；
- 为每个定理保留自然语言描述，支持搜索、复用和更清晰的证明路径。
Anthropic 说明，早期尝试曾因智能体丢失项目状态、无法有效协作而失败；这些失败尝试仍贡献了最终非样板代码的大约 7%。切换到 Prove2Me 后，项目才成功收敛。
如何验证
公开仓库使用 Lean 4.33.1 与固定版本的 Mathlib 4.33.0，默认构建目标为 FinalCheck.lean。仓库提供了多层验证：
- 从头执行
lake build，由 Lean 内核检查仓库的全部 60475 个模块；最终定理只依赖 Lean 的三个标准公理propext、Classical.choice和Quot.sound，不允许sorry、新增axiom或native_decide。 - 使用
leanprover/comparator4.33.0，将最终陈述与只依赖 Mathlib 的挑战文件比较，检查定理陈述、涉及的常量和公理集合是否一致，并通过 Lean 内核重放整个证明。 - 使用独立的 Rust Lean 内核 nanoda 0.4.13 检查导出的同一环境；仓库记录其成功检查 1052234 个声明且没有错误。项目对 nanoda 使用了四个补丁，其中一个增加进度输出，三个用于加速定义相等性搜索；仓库声明这些补丁没有增加、删除或削弱类型规则。
复核者可以按仓库说明依次运行：
git clone https://github.com/anthropics/fermats-last-theorem flt
cd flt
LEAN_NUM_THREADS=96 lake build
verification/comparator/run.sh
verification/nanoda/run.sh
完整复现的资源要求很高。仓库给出的参考数据是：构建时每个并行任务约需 5 GB 内存，.lake/ 约占 67 GB，生成的 C 文件还可能占约 220 GB；其 96 并行任务构建耗时 5 小时 32 分、内存峰值 153 GB。Comparator 运行约 14 小时 46 分、内存峰值 230 GB，因此仓库建议预留 300 GB。降低并行度可以限制内存用量，但会增加构建时间。
边界与局限
机器检查能够确认给定 Lean 陈述确实由列出的公理推导出来，但不能自动保证每个中间定理的名字准确表达其数学含义。仓库明确规定：名字与陈述不一致时，以实际 Lean 陈述为准。随仓库提供的英文摘要和推荐参考资料是自动生成的，也没有逐项人工验证。
这不是 Claude 独立发现费马大定理的新证明。成果复用了 Mathlib，以及 Imperial College London 的 FLT 项目和 flt-regular 项目中的人类开源工作；相关派生文件和署名记录已列入仓库。代码以 Apache-2.0 许可证发布，但仓库被标为研究制品，不维护且不接受贡献。
Codex 归纳：这项工作最值得关注的工程信号，是大模型、形式化证明内核、显式依赖图和可重放验证链可以协作处理超大型证明工程。它说明 AI 能显著降低形式化成本，但不等于消除了对数学解释、来源审查和独立复核的需求。
技术说明：Formalizing Fermat's Last Theorem \ Anthropic
证明仓库：GitHub - anthropics/fermats-last-theorem · GitHub