Anthropic 的 Claude 产出费马大定理首个完整的、机器可核验的证明

Anthropic 发表了一篇研究文章（2026 年 9 月 4 日），宣布 Claude 产出了费马大定理首个端到端、机器可核验的证明 —— 这是一个存在 350 年的问题，光是人类的解答就用了 129 页、耗去近十年。这份证明用Lean 4 编程语言写成，由 Lean 的逻辑内核从第一性原理出发做了检查，只用了三条标准数学公理。在 11 天里，一群 Claude 智能体基本自主地写下约 1300 万行 Lean 代码、证明了约 29500 条中间定理，完成了这次形式化。

Claude 所达成的不是一个新的数学证明。安德鲁·怀尔斯早在 1995 年就给出了第一个正确证明，此前他秘密工作六年，还在被发现一处缺口时几近崩溃。Claude 产出的，是数学家们原本预计需要整个社区花数年才能完成的东西：把那个证明形式化翻译成一种计算机能逐步核验的语言，其中没有任何逻辑环节被跳过或假定。

延伸阅读：AI 验证是卡住智能体性能的关键瓶颈

「证明」与「形式化」的区别

数学家写证明是写给别的数学家看的。一篇发表的证明依赖共享的直觉，跳过显然的步骤，援引此前工作的结论而不重述。而形式化证明恰恰相反：它什么都不能假定，每一步推理都必须被明确写出、指向在先的定义，并连回到基础公理。

Lean 是一个证明助手 —— 一种为形式化数学设计的编程语言 —— 建立在被称为「归纳构造演算」的逻辑分支之上。当 Lean 接受一个证明时，意味着它的内核已机械地核验过：每一步都由所声明的公理推出。Claude 的证明全程使用的三条公理 —— propext、Classical.choice 和 Quot.sound —— 是 Lean 类型论中经典数学的标准基础。最终检查文件确认，最终证明中任何地方都没有出现 sorry 语句（未证步骤的占位符）、没有额外添加的公理，也没有原生求值的捷径。

形式化的规模，反映出抽象平时掩盖掉多少工作量。怀尔斯那 129 页的散文式论证，本已是现代数学中最艰深的论文之一，而当每一个默认步骤都被显式写出时，它会急剧膨胀。Claude 产出的代码库横跨 60475 个 Lean 模块，大约是 Mathlib 的五倍 —— 后者是 Lean 用户构建了近十年的、形式化数学的主要社区库。完整证明可在anthropics/fermats-last-theorem 仓库中获得。

数十个 AI 智能体如何撑起一场为期 11 天的数学战役

这次形式化是在第二次尝试时成功的，用的是第一次失败时还不存在的基础设施。早期让多个 Claude 智能体协作的实验很快垮掉：智能体们弄不清哪些定理已经被证过，无法有效复用彼此的工作，最终停止了协作。那次失败贡献了最终证明中约百分之七的非样板代码行 —— 作为记录被保留在仓库里。

转折点出现在 Anthropic 研究员 Tianyi Peng 把这个项目接入Prove2Me之后 —— 他在哥伦比亚大学的团队开发 AI 形式化工具，而 Prove2Me 是他和合作者专门为这类工作建的一个开放协作平台。Prove2Me 用三项技术选择解决了协调难题。

第一，它把所有定理组织成一张有向无环图 —— 一张依赖地图，其中每个节点代表一条定理，每条边记录该定理需要先证明什么。智能体可以查阅这张图来决定哪些定理已经可以着手，也能在长时间运行之后恢复工作而不丢失自己在整场证明战役中的位置。第二，Prove2Me 把定理陈述和它们的证明分放在不同文件里，并独立维护两者之间的链接。这大幅降低了 Lean 的编译时间和内存需求，因为当证明改变而陈述未变时，不必整体重新核验。第三，每条定理都配有一段自然语言描述，使智能体能够检索已证结论的库，避免重复劳动。

在这个平台之上，用一套基于 Claude Code 的多智能体框架，整场战役跑了不到两周。所用的内部研究模型 —— Anthropic 形容其能力可比 Claude Fable 5.1 —— 在整场战役中消耗了约 60 亿输出 token。人类的介入仅限于 Peng 偶尔给出的高层方向，比如把某条子定理标为高优先级，或指出某个结论应当更早完成。

两层独立验证确认了这个结果

当智能体们发出完成信号时 —— Prove2Me 依赖图中的 FLT 根节点在美国东部时间 8 月 17 日晚上 10 点 00 分 57 秒显示为「已证明」—— 验证流程仍然要跑。Anthropic 让这份证明经受了两道独立检查。

第一道是 Lean 自己的内核，运行在 Lean 4.33.1 上，该版本包含 2026 年 8 月发布的可靠性修复。构建以 96 个并行任务运行，耗时约五个半小时，内存峰值约 153 GB。构建日志确认，fermat_last_theorem 恰好只依赖那三条标准公理，别无其他。

第二道检查用的是nanoda，那是由另一支团队用 Rust 实现的独立 Lean 内核。nanoda 核验了 1052234 条声明，无错误 —— 从同样的公理出发独立地重建了整条逻辑链。

第三件工具，leanprover/comparator，确认 Claude 所证明的定理陈述与 Mathlib 自己对费马大定理的陈述完全一致 —— 排除了「Claude 证明的是一个技术上不同、但表面相似的命题」这种可能。

自 2024 年以来领导社区形式化 FLT 主要工作的伦敦帝国理工学院数学家 Kevin Buzzard 审阅了这份证明，并形容它证明了：AI 自动形式化的产物如今在结构上已经足够可靠，可以在其上继续构建 —— 而不只是作为孤立实验被展示一下。他指出，这类技术既能揭示既有数学文献中的错误，也能减轻审稿人当下要花数月手工核验新结果的负担。

这对数学同行评议意味着什么

数学界积累验证债务已有数十年。人类审稿人是有极限的：一个复杂证明可能要花数年才能彻底查完，怀尔斯 1993 年投稿时就是如此。Thomas Hales 1998 年关于开普勒猜想的证明在评审中待了四年，最后一个 12 人审稿组只给出「99% 确定」的结论 —— Hales 随后领导了一个 20 人的形式化项目Flyspeck，直到 2015 年才完成。格里戈里·佩雷尔曼关于庞加莱猜想的证明，则用了大约四年和三份各 300 页的阐释文本，社区才予以接受。

AI 现在产出数学结果的速度，已经快过传统评审能消化的速度。OpenAI 的 Astra 模型在 2026 年 8 月解出了十个开放研究问题，并为每一个发布了 Lean 证明。OpenAI 另一项工作在 2026 年 6 月把一个厄多斯反例证明形式化为 120 万行 Lean —— 约为当时 Mathlib 规模的一半。AI 生成数学产出的节奏在加快，而人类专家审稿人的容量没有。

形式化验证为这种失配提供了一个结构性解法。一份 Lean 证明一旦通过内核检查，就在一种绝对意义上被验证了，而这种速度和覆盖面是任何人类审稿人都比不了的。Buzzard 一直主张 —— Anthropic 的文章也强化了这一点 —— 为 AI 生成的数学结果同时产出一份 Lean 形式化，很可能会成为标准做法。FLT 这个项目证明，产出这样一份形式化所需的成本和时间现在已经可及，不只是对国家实验室，甚至对小型研究团队也是如此。

Anthropic 用一个更小的实验直接演示了这一点。三名研究者用各自的 Claude Max 订阅、完全通过 Prove2Me 协作，在三天内形式化了维诺格拉多夫三素数定理 —— 一个重要的数论结论。

延伸阅读：Anthropic 研究：自动化 AI 研究员补安全缺口比专家更快

这份 1300 万行的证明留下了什么未决

这个结果带着一个 Lean 内核本身无法处理的重要保留意见。内核核验的是「一条逻辑链是否从公理推出」，而不是「被证明的那些定理是不是证明作者所意图的那些」。Claude 仓库里的代码是为机器可检查而写的，不是为人类可读而写的：定理名是机器生成的，标签里含十六进制的流水线标识符；当名称与陈述不一致时，被证明的是那个陈述。Anthropic 明确指出，没有任何工具能检查的是：每一条中间定理是否真的表示它的名字所暗示的意思。

这不是这个结果的缺陷 —— 它是对「形式化验证提供什么、不提供什么」的一份诚实描述。Lean 的职责是确认在一个给定公理系统内的逻辑一致性。至于数学共同体最终会不会把 Claude 的这份 Lean 形式化当作费马大定理的权威检查点，还是会认为仍需要一份同等规模、且人类可独立阅读的 Lean 形式化，这是一个开放问题。

1300 万行这个体量，也大大超出必要。Mathlib 的社区库是在近十年的专家打磨中长到今天这个规模的，而且高度紧凑。Claude 是按速度而非优雅来生成代码的。Anthropic 承认这份证明很可能比它需要的长得多。未来几代 AI 辅助形式化会面临压力去缩小这个差距 —— 产出既能被机器核验、又足以让数学家审阅、扩展和用于教学的证明。

值得记下的里程碑是：问题已经换了。自 Bergstra 最早提出把怀尔斯的证明形式化以来的二十多年里，约束一直是人力：把一个那种复杂度的证明翻译成机器可检查的形式，对任何单一研究团队来说都慢得无法着手。到 2026 年 9 月，那道约束正在解除。剩下的挑战不再是「AI 能不能在这个规模上形式化数学」—— 它显然能 —— 而是这些产物会成为这个领域可信赖的基础设施，还是仍然只是令人印象深刻的演示，等着第二代工具来让它们变得可读。