刚刚，Claude用11天完成费马大定理验证，清华姚班校友带队

本文来自微信公众号： APPSO ，作者：发现明日产品的

350多年的岁月里，人类一直在寻找费马大定理的答案。

1637年，法国数学家皮埃尔·德·费马在一本数学著作的页边写下一个困扰后世数百年的猜想，并留下了一句著名的话：「我发现了一个绝妙的证明，但这里的空白太小，写不下它。」

后来，人类真的找到了证明。1995年，英国数学家安德鲁·怀尔斯花费多年时间完成了费马大定理的第一个完整证明。但如今，这个数学史上的传奇问题又迎来了新的节点。

官方博客🔗https://www.anthropic.com/research/formalizing-fermats-last-theorem

就在刚刚，Anthropic公布了一项新的研究成果：Claude在几乎自主运行的情况下，用11天完成了费马大定理的首个端到端计算机验证证明。

整个过程中，Claude使用Lean编程语言构建形式化证明，生成约1300万行Lean代码，证明了超过2.95万个中间定理，最终得到了一份可以由计算机完整检查的证明。

这一次，AI做的事情并非重新发现一个数学定理，而是完成了一项过去需要数学家多年投入的工作：把人类数学中的复杂证明，转换成计算机能够逐步验证的形式。

哦，对了，伴随着GPT-6 Astra的全面开放，Anthropic刚刚也给Claude用户送上了一份「大礼包」——重置了所有Claude Max用户的每周使用额度。

一道数学难题，困住了人类3个世纪

费马大定理的问题本身非常简单。

当n大于2时，是否存在正整数a、b、c，使得aⁿ+bⁿ=cⁿ？

费马认为不存在这样的解。

然而，这个看似简单的问题，却成为数学史上最著名的难题之一。

过去几个世纪，无数数学家尝试证明它。1908年，德国哥廷根科学院甚至为解决费马大定理设立了高额奖金，仅第一年就收到621份错误证明。

直到1995年，怀尔斯才正式发表被数学界认可的证明。

不过，怀尔斯的证明远比普通数学问题复杂。

整篇论文超过100页，涉及现代数论、代数几何等多个数学领域。1993年，怀尔斯首次公布证明后，评审团队在验证过程中发现关键漏洞，他随后花费一年时间修正，最终才完成最终版本。

这件事也暴露了现代数学中的一个长期问题。

证明一个数学定理很难，验证一个复杂证明同样困难。

数学论文通常面向人类阅读，很多显而易见的推导不会逐步展开。但计算机不会默认任何步骤，每一个逻辑关系都必须被明确表达。

因此，数学界开始探索另一条道路：形式化证明。

通过Lean等证明助手，数学家可以把数学推理转换成计算机语言，让计算机自动检查证明中的每一个环节。

过去几年，数学界一直尝试将费马大定理形式化。

2024年，伦敦帝国理工学院数学家Kevin Buzzard发起相关项目，希望利用Lean完成这一任务。

按照当时的估计，这项工作可能需要多年时间。

因为怀尔斯的证明建立在几百年的数学积累之上，而计算机能够直接理解的数学知识，只占整个数学体系的一小部分。

数学家需要先将大量基础理论转换为形式化语言，再逐步搭建整个证明体系。

这是一项庞大的数学工程。而Claude的出现改变了推进速度。

证明很难，证明证明更难

这项工作的背后，是一位长期探索AI与数学交叉领域的研究者。

Tianyi Peng（彭天翼）是此次费马大定理形式化项目的重要推动者。

他本科毕业于清华大学姚班，随后在麻省理工学院完成博士研究，目前担任哥伦比亚大学商学院助理教授，同时也是Anthropic研究员。

他的研究方向长期围绕AI Agent、强化学习以及数学形式化展开。

此前，他与哥伦比亚大学团队共同开发了Prove2Me平台，希望通过多智能体协作，让AI能够参与更复杂的数学证明任务。

这项研究背后还有一个颇具意味的经历。

在本科阶段，Tianyi Peng曾完成一项数学研究成果，导师希望将相关结果纳入Nature论文。但面对导师提出的一个问题：「你是否确定这个证明完全正确？」他的回答是：「我有99%的把握，但这么长的证明很难做到100%确定。」

最终，这项成果没有进入Nature。

多年后，他选择研究数学形式化，某种程度上正是在解决当年遇到的问题：如何让复杂数学证明拥有更可靠的验证方式。

Tianyi Peng希望测试Claude是否能够帮助推进费马大定理的形式化。

让人意想不到的是，结果大大超过了预期。

在11天时间里，Claude基本自主完成了整个证明流程。为了处理如此复杂的任务，Anthropic并没有让单个AI直接完成全部工作，而是让多个Claude Agent协同合作。

这些Agent分别负责定义数学概念、证明中间定理，并利用已经完成的结果继续推进后续证明。

最终，Claude生成了约1300万行Lean代码。

这个规模远超普通数学形式化项目，相当于Lean最大数学库Mathlib规模的5倍以上。

整个过程中，Claude构建了约3.03万个定理，其中最终证明费马大定理使用了约2.95万个中间定理。

为了管理如此庞大的证明过程，Anthropic使用了一个名为Prove2Me的开放协作平台。

这个平台能够帮助AI Agent管理不同数学任务之间的关系，将复杂证明拆分成多个可以并行推进的小目标，同时记录每个定理之间的依赖关系。

结合Claude Code的多Agent工作方式，研究团队最终在不到两周时间内完成了整个形式化证明流程，总共消耗约60亿输出token。

最终结果通过Lean检查，只依赖数学基础公理，没有额外假设。

未来的数学家，可能需要同时面对人和AI

Claude完成费马大定理形式化证明的意义，并不只是速度提升。

过去，数学研究依赖同行评审确认结果是否正确。但面对越来越复杂的数学成果，人工验证正在变得越来越困难。

历史上，数学界曾多次经历漫长验证过程。

1998年，托马斯·黑尔斯证明开普勒猜想，评审团队花费多年时间审核，最终只能给出高度可信的评价。

2002年，佩雷尔曼提出庞加莱猜想证明，数学界同样花费多年时间整理和确认。

随着AI开始参与数学研究，这个问题可能更加突出。未来，AI或许能够快速生成大量数学证明，但人类研究者很难逐一阅读和验证。

形式化证明提供了一种新的可能。AI可以负责生成证明，人类负责理解思路，而Lean等系统负责检查逻辑正确性。

Anthropic认为，未来数学论文可能会同时包含面向人类阅读的解释，以及面向计算机验证的形式化证明。

这不会取代数学家的创造力，但会改变数学成果被验证和传播的方式。

过去，数学家的工作重点是提出新的理论。未来，他们可能还需要考虑如何让这些理论能够被机器理解和验证。

389年前，费马在页边留下了那份属于人类直觉的骄傲与遗憾。

而在389年后的今天，这片曾经狭窄的空白，终于被人类亲手创造的AI数字工具，填上了一份最工整、最确凿的答案。