Anthropic完成费马最后定理的Lean 4形式化证明

Anthropic公司已完成费马最后定理在Lean 4中的完整机器验证证明1。该证明基于Mathlib库，沿用Frey、Serre、Ribet、Wiles及Taylor-Wiles的经典论证路径1，采用Darmon–Diamond–Taylor 1995年阐述的方法2。

该形式化证明的代码库超过1340万行2，包含60,475个模块、29,511个定理和1,450个定义1。证明基于Lean 4.33.1和Mathlib v4.33.01，已通过两层独立验证：Lean官方验证工具leanprover/comparator v4.33.0耗时14小时46分钟完成验证，峰值内存达230GB；独立Rust内核nanoda 0.4.13检查了1,052,234个声明，未发现错误1。证明的编译耗时5小时32分钟（96个并行任务），需要67GB磁盘空间1。

这一成果标志着完成了计算机科学家Freek Wiedijk著名的100个形式化挑战清单中的最后一个定理2，该基准项目已有20年历史2。该证明仅依赖于三个标准公理：propext、Classical.choice和Quot.sound1，版权归Anthropic所有，基于Apache License 2.0发布1。

Anthropic has completed a fully machine-verified formal proof of Fermat's Last Theorem in Lean 4, marking the conclusion of Freek Wiedijk's renowned 100 Formalization Challenges benchmark after two decades.12 The proof, containing 60,475 modules with 29,511 theorems and 1,450 definitions, follows the mathematical path established by Frey, Serre, Ribet, Wiles, and Taylor-Wiles.1 Built on Lean 4.33.1 and Mathlib v4.33.0, the formalization is based on the Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument.12

The proof underwent rigorous verification through dual independent systems.1 Anthropic's internal comparator tool completed verification in 14 hours and 46 minutes using a peak of 230 GB of memory, while the independent Rust-based nanoda verifier (version 0.4.13) checked 1,052,234 declarations without error.1 The entire codebase exceeds 13.4 million lines and required 5 hours and 32 minutes to compile across 96 parallel tasks, consuming 67 GB of disk space.12 The formalization depends on only three standard axioms: propext, Classical.choice, and Quot.sound.1

Released under Apache License 2.0 with copyright held by Anthropic through 2026, the project drew on 106 files from Mathlib and incorporated work from Imperial College London's FLT project.1 According to reports, Anthropic completed this formalization in approximately 11 days using its internal AI model via the prove2.me platform.2