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

费马大定理在 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、无新增公理、无 native_decide），否则构建将失败。FinalCheck.lean 还从该定理推导出了 Mathlib 自身的陈述 FermatLastTheorem。

验证方式

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

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

第二个内核。nanoda 0.4.13，一个用 Rust 编写的独立 Lean 内核，接受了对同一环境（使用 lean4export 导出）的导出：检查了 1052234 个声明，无任何错误。我们使用自己的四个小补丁构建了 nanoda（verification/nanoda/patches/）：其中一个补丁添加了进度输出，另外三个加速了其定义相等性搜索，否则该证明中的一些声明在未修改的 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 磁盘空间，外加可在构建过程中删除的 C 文件（约 220 GB）。我们以 96 个并行任务构建耗时 5 小时 32 分钟，内存峰值达 153 GB。

comparator 约需 15 小时（我们耗时 14 小时 46 分钟），其中几乎全部时间都花在单核上的内核重放。我们的内存峰值为 230 GB，因此请预留 300 GB。请在 comparator 脚本之后运行 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 包、伽罗瓦表示、形变理论、拼接等）、flt-regular（库默定理）以及 Mathlib。ATTRIBUTION.md 列出了包含前两个项目内容的 106 个文件，注明上游文件、版权持有人和作者，以及复制 Mathlib 文本的 23 个文件（Definitions/Def_Compat_Mathlib430.lean 中的摘录和二十二个就地重新证明 Mathlib 引理的模块）。网页捆绑了 KaTeX 和 Graphviz（编译为 WebAssembly），它们依据各自的许可证发布，列于 html/assets/vendor/LICENSES.txt。Lean 和 lake-manifest.json 中的软件包在构建时获取，不在此分发。如果您发现未署名的材料，此遗漏并非有意为之。