狂干1300万行代码、消耗60亿Token。

作者 |  许丽思

编辑 |  漠影

智东西9月5日报道，今天，Anthropic公布了一项AI数学领域的新进展，Claude完成了费马大定理（Fermat's Last Theorem）首个端到端、可由计算机完整检查的形式化证明，整个过程仅用了11天。

据Anthropic披露，Claude在此期间写下约1300万行Lean代码，一共产出了约30300个可由计算机验证的定理，其中29500个中间定理进入最终证明。

最终代码量已经达到Lean核心数学库Mathlib的5倍以上，也是迄今规模最大的Lean证明项目。

这项工作的发起者，是Anthropic研究员Tianyi Peng（彭天翼）。他本科毕业于清华大学姚班，博士毕业于麻省理工学院，目前，他是哥伦比亚大学商学院助理教授、Anthropic研究员。

完成这项工作的并非一个Claude单独连续输出，而是数十个Claude Agent并行协作。整个项目消耗约60亿个输出Token，使用的是Anthropic内部一款通用研究模型，其能力大致相当于Claude Fable 5.1。

不过，Claude并不是发现一条全新的费马大定理证明路线，这次它完成的是另一件长期困扰数学界的事情，把人类数学家写给人看的证明，完整转写成机器能够逐行检查、没有逻辑跳步的形式化证明。

而这项工作，之前被认为可能需要数学家耗费数年时间。

消息一出，社交平台X上炸锅了。Google DeepMind AGI Economics负责人、芝加哥大学Booth教授 Alex Imas感慨，这是目前见过对数学领域最重要的AI成果之一，自动化形式化本身就是加速数学进展的能力。

不过，也有人觉得，AI确实完成了人类预计需要数年的形式化工程，但生成1300万行代码，这个结果远谈不上简洁。

甚至已经有网友提出，下一步能否让AI继续研究自己的证明，不断压缩1300万行代码，最终寻找更加优雅的形式化路径。

01.

困扰数学界358年的难题，

又花了30多年才让计算机真正看懂

17世纪，法国数学家费马在一本书的页边写下一个史上最著名的数学猜想之一：对于任意整数n>2，不存在正整数a、b、c，使得aⁿ+bⁿ=cⁿ。

费马当时还留下一句话：自己已经找到一个“绝妙证明”，只是页边太窄写不下。

此后超过350年，没有人能够给出正确证明。

直到1993年，英国数学家安德鲁·怀尔斯公开宣布完成证明。但两个月后的同行审查中，数学家发现其中存在关键漏洞。怀尔斯之后又花了一年时间，与Richard Taylor合作修补，最终证明于1995年正式发表。

Anthropic称，这份证明长达129页。

但人类能证明出来，并不代表计算机也能验证。

传统数学论文是写给数学家看的，大量在专业人士看来显而易见的推导会被省略。一句数学表述背后，可能依赖数十个定义、引理以及此前数百年的数学成果。

而Lean这样的证明助手就没有这种常识，每一个定义、每一次逻辑跳转、每一个中间结论，都必须被严格写出来。只要链条中有一步不能成立，Lean就不会让证明通过。

这就是所谓的数学形式化（Formalization）：将自然语言和数学符号组成的人类证明，转写为机器能够按照数学公理和逻辑规则逐步检查的程序。

2005年前后，计算机科学家已经提出将怀尔斯证明形式化的设想。2024年，伦敦帝国理工学院教授Kevin Buzzard牵头启动大型开源项目，希望使用Lean完成费马大定理的形式化证明。

这个项目原本被认为要耗时数年，结果现在，AI把进度条大幅向前推了一截。

02.

几十个Claude一起证明，

11天跑出1300万行代码

最初，Anthropic研究员彭天翼只是想测试Claude究竟能在费马大定理形式化过程中推进多远，没想到，结果超乎预期。

Anthropic称，Claude最终在11天内完成了首个端到端、经计算机检查的费马大定理形式化证明。整个过程中，人类提供的数学指导相当有限，主要是偶尔给出类似“Jacobian作为scheme优先级比较高”之类的高层方向。

但这个证明过程，一开始其实也翻车了。Anthropic发现，当多个Agent直接协作时，它们很快开始忘记整个工程进行到了哪里，一个Agent不知道其他Agent已经证明了什么，互相跟不上进度。

最终真正让系统跑起来的关键，是一套名为彭天翼团队打造的Prove2Me数学形式化协作平台。

这套平台把一个庞大的数学证明拆成一张有向无环图（DAG），最顶层是最终要证明的费马大定理，下面则不断拆分为规模越来越小的中间定理。

不同Claude Agent可以分别认领任务：有人定义数学概念，有人证明底层引理，有人继续利用已经完成的结果向上推进。

Prove2Me还会记录每个定理的自然语言说明，并允许不同Agent搜索和复用已经完成的结论。

最终，Claude一共生成了约30300个能够通过计算机验证的定理，其中约29500个进入最终证明，整套证明达到约1300万行Lean代码。

Anthropic称，最终结果通过Lean的完整检查，只使用Lean的三条最基础的标准公理。

▲克劳德・怀尔斯 (Claude Wiles) 用Prove2Me计划形式化费马大定理的关键里程碑。图中三个彩色部分分别对应克劳德在最终目标实现过程中必须证明的三个核心子定理。该图与怀尔斯最初的证明过程非常吻合。

研究团队还额外使用比较程序确认，Claude最终证明的数学命题与Mathlib中费马大定理的正式定义完全一致。

03.

带队大神，出自清华姚班

能让Claude完成这项工作的彭天翼，履历相当亮眼。

▲彭天翼

他本科毕业于清华大学姚班，早年就是信息学竞赛选手，入选过信息学奥赛国家集训队。2017年，他从清华姚班获得计算机科学学士学位，还拿下了清华大学优秀毕业论文奖。

2017年，彭天翼进入麻省理工学院继续深造，并于2023年获得博士学位。早期他主要研究量子信息、量子计算和NISQ等问题，随后研究方向逐渐转向大规模决策系统、强化学习、因果推断和实验设计。

2023年前后，他又开始进入生成式AI创业。彭天翼是Cimulate.AI创始团队成员，其个人主页称，团队从零搭建了基于Transformer和强化学习的电商搜索系统CommerceGPT。

目前，他是哥伦比亚大学商学院助理教授、Anthropic研究员，长期在哥大带领团队主攻强化学习、AI智能体以及形式化工具研发。

04.

结语：AI，正在加速改变数学研究的模式

Claude其实没有解决一个尚未被攻克的数学猜想，也没有取代怀尔斯重新证明费马大定理。真正值得关注的是，它第一次把一个规模庞大、跨越多个数学领域的证明工程，完整推进到了机器可验证的形式化阶段。

AI在数学领域的角色，也从过去的会做题，进一步进入知识整理、证明转写和结果验证这些更基础的科研流程。

过去，形式化证明高度依赖专业数学家和工程人员，周期漫长、成本高昂，因此始终难以大规模普及。

如今，大模型、多Agent协作与Lean等证明系统结合后，大规模自动形式化终于从一项高度依赖人工的耗时工程，开始向可规模化复制、工程化落地的科研基础设施演进。