机器人前瞻（公众号：robot_pro）

作者 | 许丽思

编辑 | 漠影

智东西 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 万行代码，最终寻找更加优雅的形式化路径。

一、困扰数学界 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 把进度条大幅向前推了一截。

二、几十个 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 中费马大定理的正式定义完全一致。

三、带队大神，出自清华姚班

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

彭天翼

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

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

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

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

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

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

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

过去，形式化证明高度依赖专业数学家和工程人员，周期漫长、成本高昂，因此始终难以大规模普及。如今，大模型、多 Agent 协作与 Lean 等证明系统结合后，大规模自动形式化终于从一项高度依赖人工的耗时工程，开始向可规模化复制、工程化落地的科研基础设施演进。