形式化费马大定理

我们分享费马大定理首个完整的计算机验证证明。Claude 在 11 天内基本自主地用 Lean 编程语言完成了这一证明。下文介绍形式化工作的过程，并谈谈这项工作对数学研究可能意味着什么。

约在 1637 年，皮埃尔·德·费马在他那本丢番图《算术》的页边空白处写下了一个断言，后来成为数学史上最著名的猜想之一：对于任何 n > 2，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。费马大定理（FLT）后来被证明极其难以证明。首个证明由安德鲁·怀尔斯爵士于 1995 年给出，长达 129 页，并经过数月的艰苦核查才得以确认。

十年后，荷兰计算机科学家扬·贝格斯特拉提出将怀尔斯的证明“形式化”：把数学推理转换成计算机可以自动检查的形式。此后，数学家们一直在开发编码如此复杂证明所需的方法，其中包括 2024 年由伦敦帝国理工学院的凯文·巴扎德发起的多年社区协作项目，旨在用 Lean 证明助手完成形式化工作。

最近，Anthropic 研究员田一鹏（其哥伦比亚大学团队为 AI 形式化构建工具）着手测试 Claude 能否在 FLT 形式化上取得进展。¹ 结果超出了他的预期。在 11 天内，Claude 基本自主地完成了 FLT 的首个端到端、计算机验证的证明。过程中它编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。

我们将所得证明分享给凯文·巴扎德，他表示：

自动形式化像 FLT 这样复杂的证明，是迈向未来所有数学都能被便捷验证的重要一步。随着 AI 产出越来越多的证明，轻松形式化工作的能力可以减轻评估新结果的负担（这一过程可能耗时数年）。我们期待，数学所依托的知识体系将变得更容易而非更难被信任。

与近期关于黎曼假设的 AI 驱动工作（产出了新颖的数学内容）不同，这里的新颖之处在于验证——像用计算器检查数学计算那样检查数学证明。证明数学定理需要组装复杂的逻辑链，如果其中一环断裂，后续的一切都可能不成立。要深入理解一个新结果并确信其正确性，可能需要数月甚至数年的工作。

费马大定理是一个很好的例子。² 费马在书的页边写下了定理的陈述，旁边还有一句引人遐想的注记：

我发现了一个真正奇妙的证明，但此处空白太窄，写不下。

350 多年来，一代又一代数学家寻找 FLT 的证明，无论是否“奇妙”。1908 年，有人宣布为能给出正确证明者提供 10 万德国金马克（相当于今天的 100 万至 200 万美元）的奖金，仅第一年就收到了 621 份错误尝试。

1993 年 6 月，怀尔斯在为期三天的系列讲座中展示了他认为是 FLT 首个正确证明的内容。在多位数学家进行密集核查两个月后，一位审阅者向怀尔斯提出了一个问题，暴露出一个关键漏洞。怀尔斯花了一年时间试图修复，先是独自一人，后来与他的前学生理查德·泰勒合作。他几乎要放弃时，终于意识到一个早先曾放弃的思路可以修复证明。怀尔斯于 1995 年 5 月发表了 FLT 的首个正确证明；它依赖的现代数学技术远超 1637 年费马所知的范畴。由于经过数百年尝试仍未找到初等证明，数学界现在相信费马本人所谓的“奇妙证明”是错误的。

验证证明正确性的一种方式是让计算机来做。像 Lean 这样的证明助手以算法方式验证证明的逻辑，无可置疑地展示其正确性。对人来说困难的部分在于重写证明，使 Lean 能够理解。面向人类读者的证明会跳过许多显然的步骤，而 Lean 需要看到每一步，无论多么琐碎。人类证明还建立在数百年已发表工作的基础上，而形式化只能从已形式化的极小部分数学开始。

对于 FLT，形式化过程预计需要数年。仅数学界用来描述项目初始阶段的蓝图就长达 86 页。

Claude 在 11 天内完成了证明，过程中产出了 30,300 个定理的计算机可验证证明（最终证明使用了其中 29,500 个）。数十个 Claude agent 协作定义概念、证明中间定理，并用这些定理去证明越来越难的命题。Claude 的证明有 1300 万行 Lean 代码，是该定理所依托的主要社区数学证明库 Mathlib 规模的 5 倍以上。³

Claude 的证明遵循了 Darmon、Diamond 和 Taylor 对怀尔斯证明的简化版本。来自人类的数学输入仅限于田一鹏偶尔给出的高层指示，例如：“Jacobian 作为 scheme 看起来优先级很高”，“尽快推进 Mazur 定理”。你可以在此处查看 Claude 思考过程的摘录。

Claude 在意识到自己刚刚完成什么时的思考摘录。

Claude 的多次初步尝试失败了：虽然 agent 早期取得了一些成功，但很快失去了对项目状态的把握，协作效率下降。它们失败的尝试贡献了最终证明中约 7% 的非样板代码行。

当我们改用 Prove2Me——由田一鹏及其哥伦比亚大学合作者设计的开放协作数学形式化平台——后，工作取得了成功。Prove2Me 的帮助体现在：

• 为 agent 提供共享的待办事项列表，使其能够并行工作而不互相干扰
• 自动跟踪哪些定理已被证明，哪些仍在进行中
• 允许 agent 通过共享的“标准库”构建彼此的工作成果

借助 Prove2Me 和基于 Claude Code 的多 agent 框架，一个 agent 团队在不到两周的时间内完成了证明，消耗了约 60 亿个输出 token，来自一个与 Claude Fable 5.1 大致相当的通用的内部研究模型。完成的证明由 Lean 检查；它仅使用了 Lean 的三个标准公理，一个比较器确认了定理陈述与 Mathlib 自身对 FLT 的陈述一致。

我们能够如此迅速地产出这一证明，表明现在形式化大范围的数学已成为可能，这既可以发现常见数学证明体系中的错误，也能减轻审阅新工作的负担。在审阅了 Claude 的 Lean 证明后，凯文·巴扎德告诉我们：

形式化也是人类对 AI 生成的数学结果建立信心的关键因素。随着 AI 和 AI 辅助数学家产出比以往更多的（声称的）证明，AI 辅助形式化减轻了人类审阅者的部分负担。我们预计，在面向人类读者的任何文稿旁边同时产出形式化证明将成为常态。虽然我们不认为形式化证明应取代人类可理解的阐述，但它可能是数学界跟上 AI 生成贡献的唯一可行方式。

编写 Lean 似乎也有助于 Claude 证明新颖的结果。我们近期许多由 Claude 完成的结果都在证明的同时进行了形式化，Claude 似乎利用这些部分证明来独立检查其假设，就像它编写数值模拟来确认方向正确一样。

形式化 FLT 是一个 token 密集型项目，但它也是有史以来最大的 Lean 证明。Anthropic 研究人员做了一个小实验，使用三个个人 Claude Max 订阅来形式化 Hardy-Littlewood 圆法的应用。agent 完全通过 Prove2Me 协作，仅用三天就共同完成了维诺格拉多夫三素数定理的形式化。我们认为，只要有合适的脚手架，使用消费级 AI 订阅协作形式化重大结果是可行的。

为此，Anthropic 和其他实验室最近扩大了对外部研究人员的支持——包括从事纯数学和形式化工作的数学家——提供免费和折扣订阅及研究额度。我们还为更大的科学项目提供专项资助，其中可能包括形式化其他重大定理或改进 Lean 和 Mathlib。

随着 AI 迅速改变数学研究的面貌，Anthropic 及其他地方的数学家正在思考这对他们工作的意义。然而，形式化是我们对 AI 角色感到毫无保留地积极的领域。随着形式化成为更常见的工具，我们希望它能帮助维护对数学知识共同体的信任。

我们的形式化工作是费马定理漫长历史与形式数学发展中的一小部分。安德鲁·怀尔斯与理查德·泰勒的首个完整证明是三百多年数学的集大成者，整合了格哈德·弗雷、让-皮埃尔·塞尔、肯·里贝特、巴里·马祖尔、罗伯特·朗兰兹、杰罗德·滕内尔、谷山丰、志村五郎以及安德烈·韦伊等人的思想。Claude 的证明遵循了亨利·达蒙、弗雷德·戴蒙德和理查德·泰勒的阐述。

我们的证明改编自凯文·巴扎德领导的伦敦帝国理工学院 FLT 项目和 flt-regular 项目的部分内容。Lean 和 Mathlib 本身都是各自的心血之作，收到了数百位数学家的贡献，其中许多人使用 Lean FRO 工作。我们感谢凯文·巴扎德审阅证明并提出意见。

完整证明可在 GitHub 上获取，并附有书面导览。

---

¹ 田一鹏在哥伦比亚大学的研究小组专注于 AI 数学形式化工具。

² 费马大定理的完整历史引人入胜，但此处只需简要概括。

³ Mathlib 是 Lean 数学库，包含大量已形式化的数学定义和定理。