当地时间 2026 年 9 月 4 日，Anthropic 宣布，Claude 在基本自主运行 11 天后，完成了费马大定理的首个端到端、经计算机检查的形式化证明。需要首先澄清的是，这并非 AI 独立给出了费马大定理的新数学证明，而是将安德鲁·怀尔斯于 1995 年完成的已有证明，转换为 Lean 证明助手可以逐步校验的代码形式。

此次形式化工程的规模远超常规数学库。Claude 在此过程中生成约 1300 万行 Lean 代码，证明约 3.03 万个定理，其中约 2.95 万个中间定理被纳入费马大定理的完整证明链条。最终生成的证明规模超过 Lean 生态中主要数学证明库 Mathlib 的 5 倍。整个证明由 Lean 完成检查，且仅使用 Lean 的 3 条标准公理。

被形式化的对象遵循 Darmon、Diamond 和 Taylor 对怀尔斯原始证明的简化版本，论证路线涉及 Frey、Serre、Ribet、Wiles 以及 Taylor-Wiles 的工作。技术栈基于 Lean 4.33.1 与 Mathlib v4.33.0。

项目由 Anthropic 研究人员 Tianyi Peng 发起，采用其与哥伦比亚大学合作者开发的 Prove2Me 平台。该平台以有向无环图记录定理依赖关系，支持多个 Claude 智能体并行工作，从而在 11 天内完成超大规模工程。人类研究人员提供的数学输入主要是少量高层指令，例如确定某些数学对象或定理的优先级，具体证明过程主要由 Claude 完成。

数学形式化的难点在于，人类证明常省略被认为显而易见的推导步骤，而 Lean 需要明确验证每一个逻辑环节，且数学会引用大量尚未形式化的既有成果。这也是此类形式化通常耗时巨大的原因。

整个项目消耗约 60 亿个输出 Token，使用的是一个与 Claude Fable 5.1 大致相当的通用内部研究模型，具体版本未公开。

伦敦帝国理工学院数学家 Kevin Buzzard 审阅后认为，该自动形式化成果显示 AI 辅助形式化大型数学成果已取得重要进展。沃顿商学院教授 Ethan Mollick 则注意到，证明文档中为每一步命名并标注对应 Lean 定理的写法仍带有 Claude 的文风。

完整 Lean 证明已公开在 GitHub 仓库 anthropics/fermats-last-theorem。仓库标注为研究产物，不维护且不接受贡献。

Anthropic 表示，若类似自动形式化技术扩展到更多现代数学成果，有望降低数学研究中验证新证明的人工成本，未来为面向人类的证明同时提供形式化版本可能成为常见做法。