Anthropic 开源费马大定理形式化证明：Claude 写出近 3 万个定理

Anthropic 在 GitHub 开源了费马大定理的完整机器验证形式化证明库 fermats-last-theorem。整个工程使用 Lean 4 编写，包含 29,511 个定理、1,450 个定义模块以及超过 1300 万行代码，是有史以来规模最大的 Lean 证明项目。

它不仅给出了费马大定理最终结论的证明，还把沿途证明所需的两万多个子定理全部在机内严密推演了一遍。代码库遵循 Apache 2.0 开源协议，包含完整的离线网页文档与定理依赖图，任何人都可以克隆并重新运行验证。

它是怎么做到的

该项目的证明路线严格遵循 Frey、Serre、Ribet、Wiles 以及 Taylor-Wiles 的经典数学进路。代码并非人类手工敲写，而是由 AI 智能体在人类已有的开源 Lean 代码基础上逐步生成，并把 Lean 编译器本身作为裁判反复迭代而成。

为了保证绝对严谨，整个证明在 Lean 4.33.1 和 Mathlib v4.33.0 环境下编译。项目没有任何作弊手段，全局没有使用 sorry、native_decide、unsafe 或未证明的公理，最终推导完全落在 Lean 内置的三条标准公理之上。

验证方面 Anthropic 做了双重把关。官方不仅用 Lean 自带的比对工具完成重放验证，还把导出的环境扔给了一个由 Rust 编写的独立第三方 Lean 内核 nanoda。nanoda 检查了全部 1,052,234 个声明，结果是零错误通过。

怎么跑起来与硬件门槛

如果你想在本地完整重放这套证明，需要一台高配 Linux 或 macOS 机器，目前仓库由于路径过长暂不支持 Windows。

整个构建流程对硬件性能要求极高。运行 Lake 源码编译时，每个并行任务需要大约 5 GB 内存，个别模块峰值内存达到 36 GB。在 96 线程并行下，完整构建需要耗时 5 小时 32 分钟，峰值内存占用达到 153 GB，构建过程中生成的临时 C 文件会吃掉超过 200 GB 硬盘。

随后的内核比对脚本还需要单核运行约 15 个小时，且需要预留 300 GB 内存。如果你只是想研读证明过程，完全不需要跑完整编译，直接下载仓库解压约 390 MB 的 html 文件夹，在浏览器中打开 index.html 即可离线浏览全部定理、定义和交互式依赖拓扑图。

需要说明的是，Anthropic 明确将该项目标记为不可维护的研究产物，不接受外部 PR。而且为了供机器快速校验，证明中的大部分中间命名和变量名都是算法生成的十六进制后缀，人类直接逐行肉眼阅读源码会非常吃力。

为什么重要

我们认为，这项工作最适合形式化验证研究者、数学研究人员以及从事 AI 代码生成的工程师参考。它证明了即便在代码可读性极差的情况下，AI 也能通过严谨的编译器闭环，独立啃下人类数学史上最宏大的证明工程之一。

相比以往学术界花费数年人工推进的数学形式化项目，AI 智能体配合形式化内核的暴力求解展现了惊人的工程推进效率。虽然这些代码离人类易读的高等数学教程还很远，但它彻底打通了 AI 辅助前沿科学验证的关键路径。