AIREITER看到“Claude 解决了费马大定理”这样的标题时，最该注意的是“形式化”这三个字。Anthropic 发布了一个公开的 Lean 工件，并称它可以端到端检查该定理；但它采用的数学路线仍是成熟的 Frey–Serre–Ribet–Wiles–Taylor-Wiles 论证，而不是 Claude 新发现的证明。
先把两个说法分开
狭义地说，答案是肯定的：Anthropic 发布了一个公开仓库，其中包含费马大定理（FLT）的 Lean 4 形式化，并提供了构建和验证说明。但如果把它说成 Claude 独立解决了这个著名问题，就不准确了；真正的数学突破早在几十年前就由 Andrew Wiles 和 Richard Taylor 完成。
费马大定理断言：当 n > 2 时，a^n + b^n = c^n 不存在正整数解。Wiles 的证明发表于 1995 年；Anthropic 的成果，是把这条已经确立的数学路线转化为机器可检查的工件。想了解项目背景，可以阅读 Lean Community 发布的 FLT 项目公告。
Lean 证明回答的是一个不同于非形式化论文的问题：在指定环境中，某个经过精确定义的命题是否能够从已检查的定义、依赖项和公理推出。它不能证明 AI 发明了底层数学，也不能证明定理名称一定与其描述相符。
Anthropic 实际发布了什么
Anthropic 在 2026 年 9 月 4 日发布的研究文章中称，Claude 用 11 天完成了首个端到端、由计算机检查的 FLT Lean 形式化。文章报告称，项目大约包含 1300 万行 Lean 代码、30,300 条已证明的定理声明，其中 29,500 条被用于最终证明；同时还产生了约 60 亿个输出 token。
项目使用了 Prove2Me。Anthropic 将其描述为一个维护定理声明有向无环图、并协调多个智能体的平台。Anthropic 表示，这套形式化采用了 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 相关成熟证明路线的简化讲解。
相比公告，公开的 GitHub 仓库更适合用来核验这些说法。仓库的默认目标是 FinalCheck.lean，其中的定理声明如下：
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ n仓库明确表示，这是一个不维护、也不接受贡献的研究工件。它固定使用 Lean 4.33.1 和 Mathlib v4.33.0，包含 PROOF-PATH.md，还提供了可离线浏览的定理与定义关系图 HTML 页面。
仓库的最终检查旨在确保：如果证明依赖新增公理、sorry、native_decide、unsafe 或类似的逃生舱，就会检查失败。这样一来，读者可以直接检查工件，而不必只相信截图或文字总结。
如何复现验证
认真核验时，第一步应该是使用仓库固定的环境，而不是把某个孤立的 .lean 文件复制到另一个项目里。Lean Community 的验证指南解释了原因：Lean 每月发布新版本，Mathlib 也经常变化，而且不保证向后兼容。
先固定环境，再开始构建
仓库说明，构建面向 Linux 或 macOS，需要 elan、Git、Python、GNU coreutils，以及网络连接，以便 Lake 获取并构建固定版本的依赖。仓库报告称，.lake 目录大约需要 67 GB，此外还会生成约 220 GB 的 C 文件，这些文件之后可以删除。
仓库还报告称，每个并行任务大约需要 5 GB 内存，部分模块最多需要 36 GB。在 96 个任务并行时，仓库记录的一次构建耗时 5 小时 32 分钟，峰值内存达到 153 GB。这些是仓库报告的数字，并非本文实测结果；规划资源时应把它们视为警告，而不是保证的运行时间。
选择适合自己的验证方式
- 只做检查：阅读
FinalCheck.lean、PROOF-PATH.md和ATTRIBUTION.md，不执行构建。 - 完整 Lean 构建：使用固定版本的工具链并运行
lake build。 - 独立重放：完成构建和导出后，运行 comparator 和 nanoda 脚本。
从全新克隆的仓库开始，大致流程如下：
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.sh这几个阶段各自负责不同的事情：
| 阶段 | 仓库报告的细节 | 用途 |
|---|---|---|
lake build | 60,475 个模块；报告中的 96 任务并行构建耗时 5 小时 32 分钟 | 从源代码构建项目，并让 Lean 内核检查构建中包含的声明 |
| Comparator | 报告中的一次运行耗时 14 小时 46 分钟；峰值内存 230 GB | 检查公开的定理及其引用的常量，是否与预期的 Mathlib challenge 声明一致 |
nanoda | 完成导出后，使用 16 个线程耗时约 30 分钟 | 通过一个独立编写的 Rust 内核，重放导出的环境 |
Comparator 不能替代对定理声明本身的阅读。它有助于降低项目证明了弱化命题或略有不同命题的风险。仓库中的 PROOF-PATH.md把带名称的数学步骤映射到 Lean 声明；生成的 HTML 页面则让你无需运行 Web 应用，就能查看依赖关系。
仓库还报告了第二轮检查的额外资源成本：写出一个 37.8 GB 的导出文件可能需要约 90 GB 内存，而 nanoda 流程在检查期间可能需要约 40 GB。
这些证据能证明什么，又不能证明什么
| 证据层级 | 能够确立 | 无法确立 |
|---|---|---|
| Lean 内核构建 | 提交的证明项能够在固定版本的 Lean 环境中通过类型检查 | Claude 发现了这些数学内容，或非形式化解释与每个定理名称都完全匹配 |
FinalCheck.lean 和公理检查 | 仓库的最终定理会根据报告的公理列表进行检查，并拒绝若干列出的捷径 | 如果不检查声明本身，无法确认该定理就是历史意义上的 FLT 命题 |
#print axioms 输出 | 当预期检查通过时，依赖项包含 Lean 的标准 propext、Classical.choice 和 Quot.sound，而不是隐藏的用户自定义公理 | 整个软件供应链都已经经过独立验证 |
| Comparator | 已证明结果及其引用的常量，与仓库使用的 Mathlib-only challenge 一致 | 项目中的每一条自然语言描述都清晰，或具备足够的教学性 |
| nanoda 重放 | 导出的环境被另一套用 Rust 编写的 Lean 内核实现所接受 | 导出文件、脚本或操作系统绝不可能存在任何错误 |
PROOF-PATH.md 和归属说明 | 为人类检查数学对应关系及既有来源提供一条路径 | 机器生成的定理名称无需人工审阅就能准确描述其声明 |
Lean Community 的“Did you prove it?”检查清单给出了核心原则：编译验证的是编码后的命题，而不是定理名称是否符合原本想表达的非形式化命题。对于这个工件，comparator 以及它对 Mathlib 的使用降低了这种风险，但仍不能替代对定理声明和证明路径的阅读。
这个工件真正展示了什么
这套系统产出了一份规模异常庞大的、经过正式检查的 Lean 工件。但它没有展示 FLT 的新路线、新的初等证明，也没有证明 Claude 进行了独立的数学发现。
Anthropic 表示，这份证明采用了 Wiles 路线的简化版本。仓库也明确列出了已有工作的来源：其 ATTRIBUTION.md 指出，有 106 个文件包含来自 Imperial College London FLT 项目或 flt-regular 的材料，同时还使用了 Mathlib。要准确描述这个发布的工件，就不能忽略这些来源。
项目报告称，运行期间共证明了 30,300 条定理声明，其中约 29,500 条用于最终证明；仓库则描述了 29,511 个定理页面。这些是形式化声明和依赖项，不是 29,511 个新发现的数学结果。形式化证明需要展开人类证明中可以交给专家直觉处理的隐含步骤、类型、强制转换、定义和库依赖。
仓库表示，其源文件的首要目标是通过检查，而不是方便人类阅读：名称由机器生成，P2M 等标签是流水线标签，真正权威的是声明本身，而不是名称。这正是证明路径和 comparator 与最终定理同样重要的原因。
更早的 Lean 工作也不应被混同于 2026 年的说法。一篇关于正则素数情形下费马大定理的 2023 年论文报告称，已经完成了 Kummer 正则素数定理 Case I 的完整、无 sorry 形式化，同时指出 Case II 和 Kummer 引理仍需要大量工作。一篇发表于 2025 年的修订版则将正则素数形式化描述为该较窄情形的完整证明。
| 工作 | 范围 | 实际作用 |
|---|---|---|
flt-regular 研究 | 正则素数相关结果，以及代数数论基础设施 | 较早的形式化构件和源材料 |
| Imperial FLT 项目 | 围绕 FLT 开展现代数论的长期、可复用形式化 | 库和协作基础设施 |
| Anthropic 仓库 | 声称在 Lean 4 中完成端到端 FLT 定理，并提供构建和重放检查 | 面向已检查结果的大型研究工件，而不是为长期维护设计的库 |
Imperial/Lean FLT 项目将现代数论形式化描述为一项更广泛的基础设施建设，而不只是翻译某一个定理。Anthropic 的发布更适合被理解为一份补充性证据：它展示了协调多个 AI 智能体在既有形式化生态中能够做到什么，而不是证明此前项目的目标已经失去意义。
不同诉求，对应不同程度的信任
| 你想确认的是…… | 负责任的答案是…… | 下一步 |
|---|---|---|
| Anthropic 是否真的发布了一个工件 | 是；既有官方公告，也有公开且固定版本的仓库 | 同时阅读研究文章和仓库 |
| 编码后的定理是否就是 FLT | 仓库提供了具体的定理声明、comparator 和证明路径 | 检查 FinalCheck.lean、comparator 和 PROOF-PATH.md |
| 代码能否干净构建 | 仓库记录了从零开始的构建方式，并报告了自身的构建结果 | 如果硬件条件允许，使用 Lean 4.33.1 和 Mathlib v4.33.0 重新构建 |
| Claude 是否发明了新证明 | 没有证据支持这种描述；使用的是已经确立的 Wiles/Taylor-Wiles 数学路线 | 将其描述为 AI 辅助的形式化或证明工程 |
| 这个工件是否易于维护 | 不是；仓库明确称其不维护，代码也是机器生成的 | 把它当作研究工件，而不是可以直接放入 Mathlib 的库 |
| 这是否证明了通用的数学自主性 | 不是；它展示的是在高度明确的形式化目标和大量脚手架下的表现 | 将形式化验证能力与开放式定理发现区分开 |
如果你只想了解新闻，官方发布和仓库已经足以证明项目确实存在。如果你需要进行审计，就复现固定版本的构建并检查定理声明。如果你是在评估 AI 研究，则应把智能体编排、现有库、此前的形式化工作和计算资源都纳入对整个系统的判断。
常见问题
Claude 发现了费马大定理的新证明吗？
没有。Anthropic 的工件形式化的是一条与 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 相关的成熟证明路线。它的成就在于以如此大的规模和速度产出可由机器检查的 Lean 工件，而不是提出新的数学解法。
Lean 构建成功，就等于证明了非形式化定理吗？
它证明的是：在该 Lean 环境中，编码后的命题能够从经过检查的依赖项推出。你仍然需要确认这个命题及其定义，确实对应你想要声称的那个非形式化定理。
仓库使用了 sorry 或额外公理吗？
仓库表示，其最终检查会拒绝 sorry、新增公理、native_decide、unsafe 以及其他几种类似捷径。预期的公理列表是 Lean 的三个标准公理：propext、Classical.choice 和 Quot.sound；应当亲自复现检查，而不是只依赖公告中的说法。
普通笔记本电脑能复现这个结果吗？
你或许可以查看仓库并进行部分构建，但完整验证并不是普通笔记本能够轻松承担的任务。仓库报告称，构建时峰值内存为 153 GB，comparator 最多需要 230 GB，同时还需要大量磁盘空间，因此硬件是核心限制。
要准确核验这一说法，应该从固定版本的 GitHub 工件开始，先读定理声明，再看标题，最后将结果准确描述为：一次规模庞大的、由 AI 辅助完成的已知数学形式化。