Claude 首次证明费马大定理：11 天写 1300 万行 Lean 代码，AI 完成数学史上最大自动形式化

一句话结论：Anthropic 用 Claude 在 11 天内完成了费马大定理的首个端到端机器验证证明，生成 1300 万行 Lean 代码、验证近 3 万条定理——这不是新数学发现，而是把 Wiles 1995 年的证明变成计算机可逐行验证的凭据。

AI 摘要

• 发生了什么：Claude 在 11 天内完成费马大定理的机器验证证明，规模是 Mathlib 的 5 倍多。
• 核心变化：多智能体协作从「乱套」到「可并行」，靠的是一个叫 Prove 2 Me 的定理任务树平台。
• 影响对象：数学家、AI 研究者、关注形式化验证的开发者。
• 下一步观察：这个模式能否复制到其他未形式化的重大数学定理上。

发生了什么

9 月 5 日，Anthropic 宣布 Claude 完成了费马大定理的首个端到端机器验证证明。费马大定理折磨了数学家 350 多年，Andrew Wiles 在 1995 年给出了最终证明，但那套证明长达 129 页，之后人类一直在尝试把它「形式化」——也就是翻译成 Lean 这样的计算机可验证语言，让每一行推理都能被机器逐行检查。

Anthropic 的做法是：让 Claude 在 11 天内生成 1300 万行 Lean 代码，产出了 30300 条可验证定理，其中 29500 条被采纳进最终证明。这个体量是全球最大数学定理库 Mathlib 的 5 倍多，整个过程烧掉了 60 亿 Token。

领头的，是清华姚班出身、现任哥伦比亚大学商学院助理教授兼 Anthropic 研究员的彭天翼。伦敦帝国理工学院的数学家 Kevin Buzzard 审查了这份证明，确认它「除数学公理外不依赖任何假设」即可成立。Buzzard 本人从 2024 年就带着人类团队在做同一个形式化项目，资金已落实到了 2029 年，但还没完成——Claude 用了 11 天就追上了。

核心变化

从「几十个 Agent 乱套」到 Prove 2 Me 救场

这件事最值得写的不是「AI 又证明了一个定理」，而是 Anthropic 自己披露的过程：早期让几十个 Claude 智能体协作，很快就彻底乱套了，互相跟不上进度，早期失败尝试贡献的代码最后只占了 7%。

转折点是彭天翼团队做出来的 Prove 2 Me 平台。它给每个 AI 一张清晰的「定理 DAG」（任务树），告诉它下一步该证明哪个中间节点，再配上 Claude Code 的多智能体框架，几十个智能体就能高效并行。用 Anthropic 的说法，Prove 2 Me 相当于给 AI 配了个「超级项目经理」。

数学界的态度：机器可验证，而非新发现

需要明确区分一件事：这不是「AI 发现了新的数学真理」。Claude 做的是把 Wiles 1995 年已经完成的证明「形式化」——翻译成 Lean 代码，让计算机能逐行验证。Gate 新闻引述 Buzzard 的话点得很清楚：这代表的是「对 Wiles 证明的机器可检查凭据，而不是一项新的数学发现」。

但它的意义依然重大。当前数学界有个越来越尖锐的问题：未经验证的证明（包括 AI 写的）积累速度，已经超过了人类手动检查的速度。开普勒猜想的计算机辅助证明，评审花了 4 年，评审组最后只能承诺「99% 确定」。如果 AI 能大规模自动形式化，等于给这些证明配上了机器裁判。

为什么这件事重要

对数学家：费马大定理的形式化一直是「珠穆朗玛峰」级别的目标。这个结果意味着，未来「附带形式化验证代码」可能成为论文标配——当 AI 能快速生成成千上万条新猜想时，人类看不过来，机器验证就成了刚需。这也呼应了我们之前关注的 Claude 科研进展。

对 AI 研究者：这不是单模型推理能力的展示，而是一次「多智能体协作 + 任务规划」的工程实践。关键不在模型多强，而在 Prove 2 Me 这套把大任务拆成可并行、可追踪子任务的编排方式。

对开发者：Anthropic 顺手做了个小实验——用 3 个普通账号在 Prove 2 Me 上花了 3 天，就把数论里著名的「维诺格拉多夫三素数定理」也形式化了。这暗示这套编排范式可能有一定的普适性，不限于费马大定理。

智盒判断

短期：这是一个「工程能力」而非「数学能力」的里程碑。Claude 没有「证明」费马大定理，它把已有的证明机械化验证了——但这恰好是当前 AI 最擅长的、也是最稀缺的能力：把人类难以手工完成的形式化工作规模化成真。

中期：Prove 2 Me 的定理 DAG 思路值得关注。它解决的是多智能体协作里的一个根本问题——如何让几十个 Agent 不互相踩脚、不重复劳动。这个模式如果开源或产品化，对任何「大规模、可拆解、可验证」的任务（不限于数学）都有借鉴意义。

长期：当 AI 能快速生成大量证明和猜想，人类审不过来时，「形式化验证」会成为 AI 产出的默认质量闸门。这件事和 OpenAI Astra 用 2000 美元算力解数学难题 放在一起看，指向同一个趋势：AI 正在从「会算」走向「算得让人放心」。

风险与不确定性

• 这是对 Wiles 证明的形式化，不是新数学发现，媒体标题里的「证明」容易引起误解。
• 1300 万行代码、60 亿 Token 的数字来自 Anthropic 官方，第三方独立复现还需时间。
• 彭天翼团队的 Prove 2 Me 平台目前是否开源、能否复用，官方披露信息有限。
• 形式化证明「机器可验证」不等于「人类理解」，数学理解的传播问题依然存在。

后续观察

• Prove 2 Me 平台是否会开源，以及它的多智能体编排方法能否推广到其他领域。
• 更多重大数学定理（如 ABC 猜想、黎曼猜想的已知进展）能否被类似的自动形式化流程覆盖。
• 数学界对「AI 形式化证明」的接受度和引用规范是否会随之调整。

FAQ

Claude 是真的「证明」了费马大定理吗？

严格说不是。Claude 做的是「形式化」——把 Andrew Wiles 在 1995 年已经完成的证明翻译成 Lean 代码，让计算机能逐行验证。它没有发现新的数学真理，而是给已有的证明提供了机器可检查的凭据。数学家 Kevin Buzzard 已审查确认其成立。

1300 万行代码是什么概念？

它是目前最大的 Lean 证明，规模是全球最大数学定理库 Mathlib 的 5 倍多。整个证明过程烧掉了约 60 亿 Token，用了 11 天。作为对比，人类团队从 2024 年就在做同一个形式化项目，尚未完成。

这对普通开发者有什么影响？

直接的影响不大，但它背后的「多智能体协作编排」思路值得关注——如何把一个大任务拆成可并行、可追踪的子任务，让几十个 AI 智能体高效协作而不是互相踩脚。这套方法对任何大规模可拆解任务都有借鉴意义。

参考来源

• 新智元《刚刚，Claude 首次证明费马大定理，清华姚班大神出手了》2026-09-05
• Gate 新闻《Claude AI 撰写迄今为止最长的数学证明，证明了费马大定理》2026-09-05
• Mars AI 摘要整理