Hacker News 中文摘要

RSS订阅

Lean 4 完成费马大定理的形式化证明 -- Fermat's Last Theorem in Lean 4

原文链接 | HN讨论 | 2026-09-05 16:13:24

Anthropics（anthropics）在 Lean 4 中完成了费马大定理（Fermat's Last Theorem）的完整机器检查证明，基于 Mathlib（Mathlib）构建，所用版本为 Lean 4.33.1、Mathlib v4.33.0，按 lakefile.lean 中的提交固定。证明思路沿用 Frey、Serre、Ribet、Wiles 与 Taylor-Wiles 的论证。

正文

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 用 #guard_msgs in #print axioms 把公理依赖固定为 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]；若实际公理不是这三个标准公理，构建会失败，因此不允许 sorry、额外的 axiom 或 native_decide。该文件还从这个定理推出 Mathlib 自己的陈述 FermatLastTheorem。

验证方式

  • 构建。 在 Lean 4.33.1（含 2026 年内核健全性修复）上从零执行 lake build，Mathlib 从源码编译。本仓库全部 60,475 个模块均构建成功，每个声明都经 Lean 内核检查，最终公理如上。
  • comparator。 leanprover/comparator v4.33.0 用 verification/comparator/Challenge.lean 对照构建；该文件只使用 Mathlib 陈述同一数学定理。comparator 确认被证明的陈述及其提到的每个常数都与 Challenge 文件完全一致，没有使用其他公理，并且整个证明连同 Mathlib 都能在 Lean 内核中重放。判定：Your solution is okay!
  • 另一个内核。 nanoda 0.4.13 是一个用 Rust 写的独立 Lean 内核，它接受了用 lean4export 写出的同一环境导出：Checked 1052234 declarations with no errors。我们给 nanoda 打了四个小补丁：一个加进度输出，三个加速其定义等价搜索；否则未修改的 nanoda 会被几个声明各占去数小时。补丁没有添加、删除或削弱任何类型规则。

没有任何模块含 axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def 或 #eval（Challenge.lean 有意使用 sorry，且不属于该包）。

这些检查共同确立：只要信任 Lean 内核（或 nanoda）及检查工具，上述定理确实从三个公理推出。陈述使用 Lean 内建自然数、+、≤、<、≠；唯一的 Mathlib 成分是 ℕ 上的 ^，Mathlib 将其定义为 Lean 内建的幂运算，comparator 还检查了陈述提到的每个定义都与原版 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 即可，无需服务器，可离线工作。页面只在基于 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 磁盘，另有约 220 GB 的 C 文件可在构建过程中删除。我们以 96 个任务构建，用时 5 小时 32 分，内存峰值 153 GB。
  • comparator 约需 15 小时（我们用了 14 小时 46 分），几乎全部花在单核内核重放上；内存峰值 230 GB，建议留 300 GB。随后运行 nanoda，它会复用 comparator 的工具。写 37.8 GB 导出约需 90 GB 内存、一小时；检查本身约需 40 GB（16 线程约 30 分钟）。两个脚本均面向 Linux（需 bash、git、python3、GNU coreutils；nanoda 还需 patch、cargo 与 crates.io）。

依次运行：

  • git clone <该仓库> flt && cd flt
  • LEAN_NUM_THREADS=96 lake build（默认每硬件线程一个任务；降低可限制内存）
  • verification/comparator/run.sh（判定见 .verify-work/wrapper/comparator.log 最后一行）
  • verification/nanoda/run.sh（在 comparator 后运行；判定见 .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）。部分内容源自三个 Apache-2.0 项目并已在 NOTICE 注明：Imperial College London FLT 项目（Kevin Buzzard 领导；Frey 包、Galois 表示、形变理论、patching 等）、flt-regular（Kummer 定理）与 Mathlib。ATTRIBUTION.md 列出含前两个项目材料的 106 个文件，标出上游文件、版权持有者和作者；另有 23 个文件复现 Mathlib 文本（Definitions/Def_Compat_Mathlib430.lean 中的摘录，以及 22 个原地重新证明某个 Mathlib 引理的模块）。网页捆绑了 KaTeX 和 Graphviz（编译为 WebAssembly），其许可列于 html/assets/vendor/LICENSES.txt。Lean 与 lake-manifest.json 中的包在构建时获取，不随仓库分发。若发现未注明出处的材料，属于无意遗漏。

评论

讨论整体氛围偏技术向，聚焦在形式化验证成果的价值与后续复用可能性上，部分用户表达赞赏，也有人对代码能否真正融入现有生态持保留态度。

称赞这是一项令人印象深刻的研究结果

  • 用户认为团队取得的成果非常出色，值得肯定（较多人） > 这是一项非常令人印象深刻的结果，向那个团队喝彩（@abhv）

担忧形式化代码难以直接复用于现有 Lean 库

  • 有用户指出，从经验来看，要让相关工具生成足够规范、可供社区持续维护的代码，需要大量人工调整；此次证明涉及大量前置形式化工作，希望这些基础成果不要仅服务于单个里程碑式证明，而是能被现有 Lean 库吸收复用（高赞）

有价值的补充

  • 有用户调侃，很喜欢代码中将“grind”作为关键字的设计，体现出形式化证明工具里的趣味性细节（少数人）
  • 另有用户戏称，现在终于有了费马当年试图在书页空白处写下的内容，暗指本次形式化成果与经典数学猜想的关联（少数人）