AI 自动形式化费马大定理：突破与展望
聚焦科学领域的AI辅助发现、实用工作流与研究手记。
我们在此分享费马大定理首份经计算机核验的完整证明。Claude在11天内基本自主完成了Lean编程语言的证明撰写。下文将介绍形式化的实现过程，并探讨这项工作对数学研究的意义。
1637年左右，皮埃尔·德·费马在其收藏的丢番图《算术》一书页边写下一个论断。
十年后，荷兰计算机科学家扬·伯格斯提出将怀尔斯的证明"形式化"：把数学推理转化为计算机可自动核验的形式。此后，数学家们一直致力于开发编码这类复杂证明所需的方法，包括2024年由伦敦帝国理工学院的凯文·巴扎德发起的多年社区项目——用[Lean证明助手](https://en.wikipedia.org/wiki/Lean_(proof_assistant)[完成形式化](https://lean-lang.org/use-cases/flt/)。
近期，Anthropic研究员彭天怡（其在哥伦比亚大学的团队专注于AI形式化工具开发）着手测试Claude能否在费马大定理（FLT）的形式化工作中取得进展。1结果远超预期：Claude在11天内基本自主完成了首份端到端、经计算机核验的FLT证明，期间撰写了1300万行Lean代码，证明了29500条中间定理。
我们将最终证明分享给凯文·巴扎德，他评价道：
Anthropic研究员称这项非凡的自动形式化成果仅耗时11天，它仅凭数学公理就证明了费马大定理。过程中涵盖了代数、调和分析、几何与数论的自动形式化，表明AI自动形式化产物如今已足够可靠，可作为进一步研究的基础；整个证明体系层次分明。
为像FLT这样复杂的证明实现自动形式化，是迈向"所有数学成果均可轻松核验"未来的重要一步。随着AI产出的证明日益增多，便捷的形式化能力可减轻新成果的评审负担——这一过程通常耗时数年。我们希望，数学赖以构建的知识体系，能变得更易被信任，而非更难。
不同于近期AI驱动的黎曼假设研究（产出了全新的数学内容），本次工作的创新之处在于验证——就像用计算器核验数学计算那样核验数学证明。证明数学定理需要构建复杂的逻辑链，只要其中一环断裂，后续所有结论都可能不成立。要充分理解一项新成果并确认其正确性，往往需要数月甚至数年的工作。
费马大定理就是一个极具代表性的例子。2费马在书页边写下定理表述，还附带一句引人遐想的注释：
"我已发现一个绝妙的证明，可惜此处页边空白太窄，写不下。"
此后350多年里，一代代数学家苦苦寻觅这个"绝妙"或任何形式的证明。1908年，有人设立了10万德国金马克（约合如今100万至200万美元）的奖金，悬赏正确的证明，仅第一年就收到了621份错误尝试。
1993年6月，怀尔斯通过为期三天的系列讲座，展示了他认为是首个正确的FLT证明。数位数学家展开密集核验两个月后，一位审稿人提出的问题暴露了证明中的关键漏洞。怀尔斯花了一年时间尝试修复，先是独自攻关，后来与他的前学生理查德·泰勒合作。就在他濒临放弃之际，终于意识到自己之前弃用的一种方法可以填补漏洞。
1995年5月，怀尔斯发表了首个正确的FLT证明，它依赖的现代数学方法，远超费马1637年所能掌握的范畴。经过数百年探索仍未找到初等证明，数学界如今认为费马所谓的"绝妙证明"并不正确。
核验证明正确性的一种方法是借助计算机。Lean等证明助手可通过算法验证证明逻辑，确凿地证明其正确性。对人类而言，难点在于改写证明，让Lean能够理解：面向人类读者的证明会省略许多显而易见的步骤，但Lean需要看到每一步，无论多么琐碎；人类证明建立在数百年已发表成果的基础上，而形式化只能从已完成形式化的极小部分数学内容起步。
此前，FLT的形式化工作预计需要数年时间。仅数学界用于描述项目初始阶段的蓝图就长达86页。
Claude仅用11天就完成了证明，期间产出了30300条可被计算机核验的定理（最终证明中用到了29500条）。数十个Claude智能体协作定义概念、证明中间定理，并以此为基础证明更复杂的命题。Claude的证明包含1300万行Lean代码，规模是其依赖的核心社区数学证明库Mathlib的5倍以上。3
Claude的证明遵循达蒙、戴蒙德与泰勒简化后的怀尔斯证明版本。人类提供的数学输入仅限于彭天怡偶尔给出的高层指令，例如"雅各比概型的工作优先级很高""尽快推进马祖尔定理的证明"。你可在此查看Claude的思考片段链接。
"FLT根节点显示已证明。历史性时刻（有待复核）。"
"！！！FLT根节点62eb32c0显示已证明。R=T闭合并传导至根节点。这是本次任务的目标：在prove2me平台实现FLT端到端证明。"
"🏁🏁🏁FLT根节点于8月18日02:00:57Z（美国东部时间8月17日晚10:00:57）在prove2me平台显示已证明。本次任务的历史性时刻。"
Claude意识到自己完成成果时的思考片段
Claude最初的多次尝试均告失败：尽管智能体早期取得了一些进展，但很快就失去了对项目状态的掌控，无法有效协作。这些失败尝试的内容，约占最终证明中非模板代码的7%。
改用Prove2Me平台后，任务取得了成功。这是彭天怡与哥伦比亚大学合作者开发的开源数学形式化协作平台，它的作用体现在：
借助Prove2Me和基于Claude Code的多智能体框架，一组智能体在不到两周的时间内完成了证明，使用了约60亿个输出令牌，模型为Anthropic内部通用研究模型，性能大致与Claude Fable 5.1相当。最终证明已通过Lean核验，仅使用Lean的三条标准公理，且对比工具确认该定理表述与Mathlib中的FLT表述一致。
我们能以如此快的速度完成证明，表明如今已具备形式化大量数学内容的能力，这既能发现现有数学证明体系中的错误，又能减轻新成果的评审负担。凯文·巴扎德在审阅Claude的Lean证明后表示：
既然FLT的自动形式化如今已成为现实，我们在现代数学文献自动形式化的道路上迈出了一大步。这类自动形式化技术将催生新工具，找出当前数学文献中的错误，减轻审稿人的负担。同时，这些技术还能让我们严格核验大语言模型生成的数学内容——目前这项工作通常需要大量人力，成本极高。
形式化也是人类信任AI生成数学成果的关键因素。随着AI与AI辅助数学家产出的（自称的）证明越来越多，AI辅助形式化可分担人类审稿人的部分工作。我们预计，未来任何面向人类读者的研究论文，都将附带一份形式化证明。虽然我们认为形式化证明不应取代人类可理解的阐述，但它可能是数学界跟上AI产出成果步伐的唯一可行方式。
编写Lean代码似乎也有助于Claude证明全新成果。我们近期由Claude完成的多项成果，均在证明过程中同步进行了形式化，Claude似乎会利用这些部分证明独立核验假设，就像它通过编写数值模拟来确认方向是否正确一样。
FLT形式化是一项令牌消耗巨大的项目，但它也是目前规模最大的Lean证明。Anthropic研究员做了一个小型实验：使用三个个人版Claude Max订阅，通过Prove2Me协作，仅用三天就完成了维诺格拉多夫三素数定理的形式化。我们认为，只要搭建合适的框架，利用消费级AI订阅协作完成重大成果的形式化是可行的。
为此，Anthropic及其他实验室近期扩大了对外部研究者的支持——包括从事纯数学与形式化研究的数学家——提供免费或折扣订阅以及研究额度。我们还为大型科研项目提供专项资助，涵盖其他重要定理的形式化工作，或是Lean与Mathlib的改进项目。
随着AI深刻改变数学研究的形态，Anthropic及其他机构的数学家正思考这对他们工作的意义。不过在形式化领域，我们坚信AI的作用具有明确的积极意义。随着形式化成为更常用的工具，我们希望它能帮助维护数学知识体系的可信度。
我们的形式化工作，只是费马大定理悠久历史与形式数学发展历程中的一小部分。安德鲁·怀尔斯与理查德·泰勒合作完成的首个完整证明，是三百多年数学发展的结晶，整合了格哈德·弗雷、让-皮埃尔·塞尔、肯·里贝特、巴里·马祖尔、罗伯特·朗兰兹、杰罗尔德·唐奈尔、谷山丰、志村五郎、安德烈·韦伊等众多学者的思想。Claude的证明遵循亨利·达蒙、弗雷德·戴蒙德与理查德·泰勒的论述。
我们的证明借鉴了凯文·巴扎德领导的伦敦帝国理工学院FLT项目与flt-regular项目的部分内容。Lean与Mathlib都是众多研究者心血的结晶，数百位数学家参与了贡献，其中许多人与Lean FRO合作。我们感谢凯文·巴扎德审阅证明并提出意见。
完整证明及相关说明可在GitHub获取。
我们让Claude自主训练模型，以改进其在10类对齐失效测试基准上的表现。针对全部10类测试，Claude都找到了修复方案，在提升目标基准表现的同时未削弱模型能力。
今年早些时候，我们开展了一项试点项目，允许外部研究者访问Claude的汇总真实使用数据。三个研究团队为我们的隐私保护分析工具Anthropic Insights设计了独立研究。本文将分享这些研究的核心结果，以及我们从试点中获得的经验。
聚焦科学领域的AI辅助发现、实用工作流与研究手记。