费马大定理被 Lean 4 完整机器验证：Anthropic 开源全程可机检的证明

人类数学史上最著名的定理之一——费马大定理，如今有了一份「机器可验证」的完整证明。Anthropic 在 GitHub 开源了 fermats-last-theorem：一个在 Lean 4 中完成的、可由形式化证明系统逐行检查的怀尔斯（Wiles）式证明，并声称已通过两个相互独立的证明内核校验。

这是什么

简单说：这是用 Mathlib（Lean 4 的数学库，版本 v4.33.0，按 lakefile.lean 锁定提交）把「费马大定理」的完整证明写成一段段机器可读的形式化代码。核心结论写在 Theorems/Thm_fermat_last_theorem.lean 里：

~~~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

~~~

即：对任意整数 n ≥ 3，不存在正整数 a、b、c 满足 a^n + b^n = c^n——这正是费马在 1637 年提出的猜想，1995 年由安德鲁·怀尔斯（连同 Richard Taylor）证明，本次被完整改写成 Lean 形式。论证路线沿用经典的 Frey–Serre–Ribet–Wiles–Taylor–Wiles 思路，PROOF-PATH.md 逐条列出了每一步及其对应的 Lean 定理。

关于这个项目，应当说明几点：

这是研究产物（research artifact）：官方明确标注不维护、不接受贡献，仅供查看与验证。

它不依赖任何 sorry、手动 axiom 或 unsafe 手段，属于「干净」证明。

代码中的大量名称（如 P2M、十六进制后缀）是流水线自动化生成的标签，不代表数学含义——以定理陈述为准。

如何确保「真的证明了」

形式化证明最大的卖点是可机检，但这份代码做了更严格的多重验证：

本源构建：从零执行 lake build（Lean 4.33.1，含 2026 内核健全性修复），Mathlib 从源码编译，仓库全部 60475 个模块逐一声明通过 Lean 内核检查。

基准对照：用 leanprover/comparator v4.33.0 对照挑战目标，确认被证定理与所用每个常量都同 Mathlib 一致、无额外公理。判定：Your solution is okay!

第二内核复检：用 Rust 编写的独立 Lean 内核 nanoda 0.4.13 接受同一环境导出结果——Checked 1052234 declarations with no errors（作者对 nanoda 打了 4 个小补丁加速定义等价搜索，未削弱任何类型规则）。

全仓库没有出现 axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def 或 #eval。FinalCheck.lean 还加了一道护栏：改用 #print axioms 断言该定理只依赖 Lean 的三个标准公理（propext、Classical.choice、Quot.sound），一旦引入额外公理构建即失败。

如何亲自浏览与验证

如果你想把这份超长证明读一遍或亲自复现，项目提供了两种路径：

离线网页版：仓库内 html/ 目录（约 390 MB）把整个证明做成了静态网页，可离线浏览——每一步、每条定理（共 29511 条）、每个定义模块都有独立页面、依赖关系图与搜索框。打开 html/index.html 即可，无需 Web 服务器。

本地复现：需要 Linux 或 macOS（部分路径在 Windows 下过长）、elan 和联网能力。构建开销相当大——lake build 满负荷约需 5GB 内存/并行任务（个别模块高达 36GB）、磁盘预留 67GB，作者实测（96 并行）耗时 5 小时 32 分、峰值内存 153GB；随后 comparator 约 15 小时、nanoda 约半小时。

git clone https://github.com/anthropics/fermats-last-theorem flt && cd flt
LEAN_NUM_THREADS=96 lake build
verification/comparator/run.sh
verification/nanoda/run.sh

一点思考

这个项目最直观的意义，是把「现代数学最深证明之一」交给机器做了彻底的完整校验——任何一处隐藏的逻辑漏洞都会被形式化内核当场揪出。它同时也展示了形式化验证正在走向「消化大型经典证明」的新阶段：以人类写就的开源 Lean（Imperial College London FLT 项目、flt-regular、Mathlib）为基础，由 AI 代理产出形式化封装、再由 Lean 系统仲裁真伪。

它的局限也很直白：校验工具能证明「在该陈述下方的一切都严密」，却无法替读者判断每个中间定理是否真的表达了它所声称的含义。这正是 PROOF-PATH.md 和可浏览 html/ 存在的意义——把「机器说它成立」与「人类看懂它为何成立」两件事尽量拉近。

项目以 Apache-2.0 协议发布，部分内容源于三个同为 Apache-2.0 的开源项目（详见 NOTICE 与 ATTRIBUTION.md 中的逐文件归属）。想一睹「数学 + AI + 形式化验证」结合的产物，这份仓库值得收藏一眼。