# 费马大定理的 Lean 4 机器检查完整证明开源发布

- 来源：Hacker News 热门（buzzing.cc 中文翻译）
- 作者：aaraujo002
- 发布时间：2026-09-05 15:56
- AIHOT 分数：79
- AIHOT 标记：已收录
- AIHOT 链接：https://aihot.news/items/cmto3hqh80160roxt5aweoxun
- 原文链接：https://github.com/anthropics/fermats-last-theorem

## AI 摘要

Anthropic 发布基于 Lean 4.33.1 和 Mathlib 的费马大定理完整机器检查证明，遵循 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 的论证路线，以 Apache 2.0 开源。

## 正文

费马大定理在 Lean 4 中的证明

在 Lean 4 中，基于 Mathlib（Lean 4.33.1；Mathlib v4.33.0，通过 lakefile.lean 中的提交固定版本），给出了费马大定理的一个完整的、机器校验的证明。其论证思路来自 Frey、Serre、Ribet、Wiles 以及 Taylor-Wiles。PROOF-PATH.md 标出了每一步及其所对应的 Lean 定理，html/ 文件夹则以网页形式呈现整个证明，方便离线浏览（参见下文“在浏览器中阅读证明”）。

研究产物。不进行维护，也不接受贡献。

命题陈述

Theorems/Thm_fermat_last_theorem.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

默认构建目标 FinalCheck.lean 包含

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms fermat_last_theorem

因此，除非该证明恰好仅依赖 Lean 的三个标准公理（无 sorry、无新增的 axiom、无 native_decide），否则构建将失败。FinalCheck.lean 还从该定理推导出了 Mathlib 自身的陈述 FermatLastTheorem。

验证方式

构建。 在 Lean 4.33.1（包含 2026 年内核健全性修复）上从零开始进行 lake build，Mathlib 从源码编译。该仓库的全部 60,475 个模块均成功构建，每个声明都经过 Lean 内核检查，公理情况如上所述。

comparator. leanprover/comparator v4.33.0 针对 verification/comparator/Challenge.lean 检查了构建结果，后者仅使用 Mathlib 就陈述了该定理。它确认了所证明的命题及其提到的每个常量都与挑战完全一致，没有使用其他公理，并且整个证明（包括 Mathlib 在内）都能在 Lean 内核中完整重放。结论：Your solution is okay!

第二个内核。 nanoda 0.4.13 是一个用 Rust 编写的独立 Lean 内核，它接受了对同一环境（使用 lean4export 导出）的导出结果：Checked 1052234 declarations with no errors。我们使用自己的四个小补丁（verification/nanoda/patches/）构建了 nanoda：其中一个补丁用于添加进度输出，另外三个用于加速其定义相等性搜索，否则该证明中的一些声明在未修改的 nanoda 上每个都需要占用数小时。这些补丁均未添加、删除或削弱任何类型规则。

没有任何模块包含 axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def 或 #eval（Challenge.lean 按设计使用了 sorry，且不属于该软件包的一部分）。

综合这些检查，可以确认：在信任 Lean 内核（或 nanoda）及检查工具的前提下，上述命题可由三条公理推出。该命题使用 Lean 内置的自然数、+、≤、< 和 ≠ 书写；其中唯一用到的 Mathlib 成分是 ℕ 上的 ^，Mathlib 将其定义为 Lean 内置的幂运算，而比较器会检查命题中提到的每个定义是否与标准 Mathlib 完全一致。Mathlib 中的其他内容无需信任，因为内核会检查命题之下的所有内容。没有任何工具能检查的是：每个中间定理是否名副其实；这需要读者自行判断，而 PROOF-PATH.md 标明了每一步背后的 Lean 定理，并精确说明了每个被引用的经典结论在此处证明中的强度。

在浏览器中阅读证明

html/ 文件夹（约 390 MB）以静态网页形式呈现此仓库：逐步展示证明路径；为 29,511 条定理各设一个页面（精确的 Lean 语句、它引用了什么以及什么引用了它，还有可展开的依赖关系图），并为 1,450 个定义模块各设一个页面（完整源码以及哪些语句使用了它）；提供覆盖所有定理和定义名称的搜索框；以图形方式展示里程碑式定理；以及带有交叉链接渲染的 README.md、PROOF-PATH.md 和 ATTRIBUTION.md。该文件夹属于此仓库的一部分，因此克隆或 ZIP 下载已包含它（如果您以单独的压缩包获取 html/，请将其解压到仓库根目录）。在网页浏览器中打开 html/index.html；一切均可离线运行，无需 Web 服务器。这些页面仅在基于 Chromium 的浏览器中经过机器测试，html/README-DOCS.md 说明了哪些内容引自 Lean 文件、哪些是生成的（英文摘要和建议的参考文献为自动生成；Lean 语句具有权威性）。

自行验证

您需要 Linux 或 macOS（某些路径对 Windows 来说太长）、elan（它会从 lean-toolchain 安装 Lean 4.33.1），以及网络连接：Lake 会从 GitHub 获取 Mathlib 并从源码编译，因为没有预构建的 Mathlib 与此工具链匹配（在 96 个并行任务下约需 13 分钟）。

构建每个并行任务约需 5 GB 内存（少数模块需要高达 36 GB）；.lake/ 下约需 67 GB 磁盘空间，外加可在构建过程中删除的 C 文件（约 220 GB）。我们以 96 个并行任务构建耗时 5 小时 32 分钟，内存峰值达 153 GB。

比较器大约需要 15 小时（我们的耗时：14 小时 46 分钟），其中几乎全部时间都花在单核上的内核重放。我们的峰值内存为 230 GB，因此建议预留 300 GB。在比较器脚本之后运行 nanoda，它会复用该脚本的工具。写入 37.8 GB 的导出文件大约需要 90 GB 内存，耗时约一小时；而检查本身约需 40 GB 内存（16 线程下约 30 分钟）。两个脚本均面向 Linux（bash、git、python3、GNU coreutils；nanoda 还需要 patch、cargo 和 crates.io）。

git clone <this repository> flt && cd flt LEAN_NUM_THREADS=96 lake build # one job per hardware thread by default; lower it to bound memory (about 5 GB per job) verification/comparator/run.sh # verdict: last line of .verify-work/wrapper/comparator.log verification/nanoda/run.sh # after the comparator script; verdict: .verify-work/nanoda/run-*/nanoda.stdout

Lean 在构建过程中会打印大量弃用警告和风格检查器警告。它们不影响结果。当输出以 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] 和 Build completed successfully 结尾时，即表示构建成功。每个脚本都会获取并构建其固定版本的检查器，成功时以退出码 0 结束。

关于源码

FinalCheck.lean 是默认目标；Theorems/ 存放命题，P2M/Sol/ 存放证明（每个证明都导入其所引用的命题），Definitions/ 存放定义，verification/ 存放两项检查，html/ 存放上文所述的网页，tools/docs-site/ 存放生成这些网页的程序。Lean 源码由 AI 智能体在人工编写的开源 Lean 基础上生成，以 Lean 作为仲裁者，其编写目的是供检查而非阅读：名称由机器生成，诸如 P2M 之类的标签或十六进制后缀是流水线标签而非数学内容；当名称与命题不一致时，以命题为准（即实际被证明的内容）。除上游声明、文档字符串和引用（列于 ATTRIBUTION.md）以及 #guard_msgs 所检查的预期输出注释外，其余注释均已移除。

许可与署名

版权所有 2026 Anthropic, PBC；依据 Apache License 2.0 许可发布（LICENSE）。部分内容源自 NOTICE 中致谢的三个 Apache-2.0 项目：由 Kevin Buzzard 领导的 帝国理工学院 FLT 项目（Frey 包、伽罗瓦表示、形变理论、patching 等）、flt-regular（Kummer 定理）以及 Mathlib。ATTRIBUTION.md 列出了包含前两个项目内容的 106 个文件，注明上游文件、版权持有人和作者，以及复现 Mathlib 文本的 23 个文件（Definitions/Def_Compat_Mathlib430.lean 中的摘录和二十二个就地重新证明 Mathlib 引理的模块）。网页捆绑了 KaTeX 和 Graphviz（编译为 WebAssembly），它们依据各自的许可证发布，列于 html/assets/vendor/LICENSES.txt。Lean 及 lake-manifest.json 中的包在构建时获取，不随本分发提供。如果您发现未注明出处的材料，该遗漏并非有意为之。