Anthropic 模型用 Lean 形式化费马大定理，1340 万行代码完成 20 年基准收官

marc_lelarge · x · 2026-09-05

Anthropic 内部模型借助 prove2.me 平台，在 Lean 中完整形式化了费马大定理（FLT）的证明，这是 Freek Wiedijk 著名「100 个形式化挑战」清单的最后一项，为这一 20 年的基准画上句号。

数学家 Kevin Buzzard 所在的 Xena 项目博主亲自编译并运行了校验器，确认代码可以通过。
证明走的是 Wiles–Taylor 论证的 Darmon–Diamond–Taylor（1995）路线，涉及 Fontaine 理论与 Mazur 的 Eisenstein 理想工作；对奇正则素数的情形此前已被形式化（最小非正则素数 37），因此结论完整。
代码库超过 1340 万行，在 96 核机器上编译耗时约为 Lean 数学库 mathlib 的 20 倍，探索时需借助 Anthropic 提供的 HTML 文档。
作者感叹自己此前的 FLT 形式化项目被 Anthropic「抢先完成」。

「模型」频道最新