费马大定理在 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 中的软件包在构建时获取，不在此分发。如果您发现未署名的材料，此遗漏并非有意为之。
Fermat's Last Theorem in Lean 4
A complete, machine-checked proof of Fermat's Last Theorem in Lean 4, built on Mathlib (Lean 4.33.1; Mathlib v4.33.0, pinned by commit in lakefile.lean). The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles. PROOF-PATH.md names each step and the Lean theorem that carries it, and the html/ folder presents the whole proof as web pages you can browse offline (see "Reading the proof in a browser" below).
Research artifact. Not maintained and not accepting contributions.
The statement
Theorems/Thm_fermat_last_theorem.lean declares
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
and the default build target FinalCheck.lean contains
/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
so the build fails unless the proof rests on exactly Lean's three standard axioms (no sorry, no added axiom, no native_decide). FinalCheck.lean also derives Mathlib's own statement, FermatLastTheorem, from this theorem.
How it was verified
- Build. A from-scratch
lake buildon Lean 4.33.1 (which includes the 2026 kernel soundness fixes), with Mathlib compiled from source. All 60,475 modules of this repository built, every declaration was checked by the Lean kernel, and the axioms are as above. - comparator. leanprover/comparator
v4.33.0checked the build againstverification/comparator/Challenge.lean, which states the theorem using only Mathlib. It confirmed that the proved statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the whole proof, Mathlib included, replays through the Lean kernel. Verdict:Your solution is okay! - A second kernel. nanoda 0.4.13, an independent Lean kernel written in Rust, accepted an export of the same environment (written with lean4export):
Checked 1052234 declarations with no errors. We built nanoda with four small patches of our own (verification/nanoda/patches/): one adds progress output and three speed up its definitional-equality search, without which a few declarations of this proof occupy unmodified nanoda for many hours each. None of the patches adds, removes or weakens a typing rule.
No module contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def or #eval (Challenge.lean uses sorry by design and is not part of the package).
Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools. The statement is written with Lean's built-in natural numbers, +, ≤, < and ≠; its one Mathlib ingredient is ^ on ℕ, which Mathlib defines as Lean's built-in exponentiation, and comparator checks that every definition the statement mentions is identical to stock Mathlib's. Nothing else in Mathlib has to be trusted, because the kernel checks everything beneath the statement. What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge, and PROOF-PATH.md names the Lean theorem behind each step and states exactly how strong each named classical result is as proved here.
Reading the proof in a browser
The html/ folder (about 390 MB) presents this repository as static web pages: the route of the proof step by step; a page for each of the 29,511 theorems (the exact Lean statement, what it cites and what cites it, and an expandable dependency graph) and for each of the 1,450 definition modules (the full source and which statements use it); a search box over all theorem and definition names; the landmark theorems as a graph; and README.md, PROOF-PATH.md and ATTRIBUTION.md rendered with cross-links. The folder is part of this repository, so a clone or a ZIP download already contains it (if you obtained html/ as a separate archive, unpack it at the repository root). Open html/index.html in a web browser; everything works offline, with no web server. The pages were machine-tested in a Chromium-based browser only, and html/README-DOCS.md explains what is quoted from the Lean files and what is generated (the English summaries and suggested references are generated automatically; the Lean statement is authoritative).
Check it yourself
- You need Linux or macOS (some paths are too long for Windows), elan (it installs Lean 4.33.1 from
lean-toolchain), and a network connection: Lake fetches Mathlib from GitHub and compiles it from source, since no prebuilt Mathlib matches this toolchain (about 13 minutes at 96 jobs). - The build needs about 5 GB of memory per parallel job (a few modules need up to 36 GB); about 67 GB of disk under
.lake/, plus C files (about 220 GB) that can be deleted as the build goes. Ours took 5 h 32 min at 96 jobs, with a peak of 153 GB of memory. - comparator takes about 15 hours (ours: 14 h 46 min), nearly all of it the kernel replay on one core. Our peak memory was 230 GB, so allow 300 GB. Run nanoda after the comparator script, whose tools it reuses. Writing the 37.8 GB export takes about 90 GB of memory for an hour, and the check itself about 40 GB (about 30 minutes at 16 threads). Both scripts are for Linux (bash, git, python3, GNU coreutils; nanoda also needs
patch,cargoand 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 prints a large number of deprecation and style-linter warnings while building. They do not affect the result. The build has succeeded when its output ends with 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] and Build completed successfully. Each script fetches and builds its checker at a pinned version and exits 0 on success.
About the sources
FinalCheck.lean is the default target; Theorems/ holds the statements, P2M/Sol/ the proofs (each importing the statements it cites), Definitions/ the definitions, verification/ the two checks, html/ the web pages described above and tools/docs-site/ the program that generated them. The Lean sources were produced by AI agents building on human-written open-source Lean, with Lean as the arbiter, and are written to be checked rather than read: names are machine-generated, labels such as P2M or hexadecimal suffixes are pipeline labels rather than mathematics, and where a name and a statement disagree the statement is what was proved. Comments were removed, apart from upstream notices, doc strings and citations (listed in ATTRIBUTION.md) and the expected-output comment that #guard_msgs checks.
Licence and attribution
Copyright 2026 Anthropic, PBC; released under the Apache License 2.0 (LICENSE). Portions derive from three Apache-2.0 projects credited in NOTICE: the Imperial College London FLT project led by Kevin Buzzard (Frey package, Galois representations, deformation theory, patching and more), flt-regular (Kummer's theorem) and Mathlib. ATTRIBUTION.md lists the 106 files containing material from the first two, with upstream file, copyright holder and authors, and the 23 files that reproduce Mathlib text (the excerpts in Definitions/Def_Compat_Mathlib430.lean and twenty-two modules that re-prove a Mathlib lemma in place). The web pages bundle KaTeX and Graphviz (compiled to WebAssembly) under their own licences, listed in html/assets/vendor/LICENSES.txt. Lean and the packages in lake-manifest.json are fetched at build time, not distributed here. If you recognise unattributed material, the omission is unintentional.