---
title: Anthropic 称 Claude 写出费马大定理的完整 Lean 证明
dek: Anthropic 于 2026 年 9 月 4 日表示，Claude 智能体用 11 天写出了费马大定理的完整 Lean 证明，代码约 1300 万行。证明已经公开，配套文档列出了它通过的各项检查，以及重复这些检查所需的计算资源。
disclosure: 调研和起草本简报的程序基于 Anthropic 的 Claude 模型构建。本简报的报道对象是 Anthropic。
---
Anthropic 于 2026 年 9 月 4 日表示，Claude 基本自主地工作了 11 天，写出了费马大定理的证明。公司称，这是该定理首个经计算机检验的完整证明。证明用 Lean 写成。Lean 是一种证明助手，也就是能逐步检查证明的软件。[^1]

据 Anthropic 介绍，数十个 Claude 智能体写下约 1300 万行 Lean 代码，证明了约 29,500 个中间定理，供最终证明使用。这些智能体使用的是一个内部模型，公司称该模型大致相当于 Claude Fable 5.1。证明沿用的是 Henri Darmon、Fred Diamond 和 Richard Taylor 对 Andrew Wiles 证明的简化版本。Anthropic 称，人类在数学上的参与仅限于其研究员 Tianyi Peng 偶尔给出的高层指示。智能体通过 Prove2Me 协同工作，这一平台由 Peng 在哥伦比亚大学的研究组开发。这份证明还改编了伦敦帝国理工学院一个项目的部分内容。该项目由 Kevin Buzzard 领导，目标是把这一定理形式化，即写成经计算机检验的证明。[^1]

证明已在 GitHub 上公开。按默认设置，只要定理依赖了 Lean 三条标准公理以外的公理，构建就会失败。根据 README，Lean 的内核检查了每一条声明。内核是 Lean 中负责接受或拒绝证明的核心程序。README 还称，comparator 工具确认所证明的命题与一条参考命题相符，后者用 Lean 的主要数学库 Mathlib 写成。第二个独立内核 nanoda 在打上补丁后也接受了这一证明，Anthropic 称这些补丁不会改变它的类型规则。README 称，只要信任这些内核和检查工具，上述检查就确立了最终定理。但它也指出，没有任何工具能检查每个中间定理的含义是否与其名称相符。重复这些检查对计算资源要求很高。Anthropic 以 96 个并行任务运行构建，耗时约五个半小时；运行 comparator 耗时近 15 个小时，内存峰值达 230 GB。[^2]

Buzzard 于 9 月 4 日撰文称，他已编译代码并运行了 comparator，结果没有问题。他补充说，这项工作在数学上基本没有给数论学家带来新东西，因为他们原本就信任这一证明，而这次形式化遵循的也是该证明的早期文献。他写道，这项工作的意义在于展示了自动形式化能够做到什么。[^3]

:::analysis
用 Lean 写成的证明，把信任从人类审稿人转移到两样东西上：检查软件，以及形式化命题，也就是用 Lean 写出的定理。在这项工作中，comparator 把命题与 Mathlib 的定义对应起来，两个独立内核也都接受了证明。因此，剩下的信任主要落在这些工具上。完整重复检查需要 200 GB 以上的内存，这意味着并非人人都有条件独立完成。
:::

:::checked
我们于 2026 年 10 月 20 日阅读了 Anthropic 的文章、该证明 GitHub 仓库的 README 和提交历史，以及 Buzzard 在 Xena 博客上的文章。我们没有自行构建证明，也没有运行 comparator 或 nanoda。Anthropic 给出的 Lean 代码量约为 1300 万行，Buzzard 的文章则称超过 1340 万行。
:::