费马大定理在 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 中的包在构建时获取，不随本分发提供。如果您发现未注明出处的材料，该遗漏并非有意为之。
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.