费马大定理首个可由机器验证的证明用了 11 天：1300 万行代码，3 万条定理

Anthropic 在一篇 9 月 4 日的研究文章中宣布，其模型 Claude 用 Lean 语言给出了费马大定理首个端到端、可由计算机验证的证明。该证明遵循安德鲁·怀尔斯 1995 年发表证明的简化版本。

这一定理提出于 17 世纪，直到 350 多年后的 1995 年才由怀尔斯首次证明。而形式化是另一件事：把数学推理转换成 Lean 这类证明助手能够逐行检查的形式。

数字

• 1300 万行 Lean 代码
• 证明了 30,300 条定理，其中 29,500 条用于最终证明
• 耗时 11 天
• 消耗约 60 亿输出 token

Anthropic 将所用模型描述为“一个大致可与 Claude Fable 5.1 相比的通用内部研究模型”。完整证明已在 GitHub 上公开。

人的部分

项目由 Tianyi Peng 发起，他是 Anthropic 的研究员，其在哥伦比亚大学的团队开发面向 AI 形式化的工具。据 Anthropic 称，“来自人类的数学输入仅限于 Tianyi 偶尔给出的高层指示”。

完成后的证明由伦敦帝国理工学院的 Kevin Buzzard 审阅，他所在的社区自 2024 年起便在做这一定理的形式化。该工作还借助了 Prove2Me，一个由 Peng 及其哥大合作者设计的数学形式化开放协作平台。

Anthropic 强调，这项工作建立在“三个世纪数学家的成果，以及数百位 Lean 与 Mathlib 贡献者的努力”之上。

公司自己写下的限度

Anthropic 明确写出一个限度：Claude 的证明体量超过 Mathlib 的五倍，并且“很可能远比它需要的更长”。也就是说，产出的并非最优雅的证明，而是一份完整、可运行、机器能够验证的证明。

为何重要

核验一份大型数学证明是否正确，可能需要数年。形式化把这份负担交给计算机：证明一旦被翻译成 Lean，其正确性即可由机器验证。Anthropic 将此呈现为一个步骤，用以减轻“在证明产出前所未有之多的时代里，数学审稿的负担”。

沿途证明的 2.9 万余条定理是另一项收获，它们位于此前从未被形式化的数学领域，如今成为后续形式化工作的基础。