狂干 1300 万行代码、消耗 60 亿 Token。
智东西 9 月 5 日报道，Anthropic 公布 AI 在数学领域的重大突破：Claude 完成了费马大定理（Fermat's Last Theorem）首个端到端、可由计算机完整检查的形式化证明，全程仅耗时 11 天。
据披露，Claude 在此期间生成约 1300 万行 Lean 代码，产出 30300 个可验证定理，其中 29500 个进入最终证明。该代码量超 Lean 核心数学库 Mathlib 的 5 倍，创下迄今最大规模 Lean 证明项目纪录。
项目由 Anthropic 研究员、哥伦比亚大学商学院助理教授 Tianyi Peng（彭天翼）发起。其本科毕业于清华大学姚班，博士毕业于麻省理工学院。
此次任务并非单一大模型连续输出，而是数十个 Claude Agent 并行协作完成。项目消耗约 60 亿输出 Token，所用模型能力大致相当于 Claude Fable 5.1。
Claude 并未发现新的证明路线，而是将人类数学家撰写的自然语言证明，完整转写为机器可逐行检查、无逻辑跳步的形式化证明。这项工作此前被认为需耗费数学家数年精力。
消息引发业界轰动。Google DeepMind AGI Economics 负责人 Alex Imas 评价称，这是数学领域最重要的 AI 成果之一，自动化形式化将加速数学进展。
亦有观点指出，虽然 AI 完成了预计需数年的人工工程，但 1300 万行代码略显冗余。网友建议下一步可利用 AI 压缩代码，寻找更优雅的形式化路径。
01. 困扰数学界 358 年的难题，又花了 30 多年才让计算机真正看懂
17 世纪，法国数学家费马提出猜想：对于任意整数 n>2，不存在正整数 a、b、c 使得 aⁿ+bⁿ=cⁿ。尽管费马声称有“绝妙证明”，但该猜想此后 350 余年无人能证。
直到 1995 年，英国数学家安德鲁·怀尔斯与 Richard Taylor 合作修补漏洞后，正式发表长达 129 页的证明。
然而，人类可读的证明不代表计算机可验证。传统数学论文常省略显而易见的推导，而 Lean 等证明助手要求每一个定义、逻辑跳转及中间结论均被严格写出，任何一步不成立即无法通过。
这便是数学形式化（Formalization）：将人类证明转写为机器可按公理和逻辑规则逐步检查的程序。自 2005 年提出设想至 2024 年伦敦帝国理工学院启动开源项目，该过程原定耗时数年，如今被 AI 大幅加速。
02. 几十个 Claude 一起证明，11 天跑出 1300 万行代码
Anthropic 研究员彭天翼最初旨在测试 Claude 在形式化过程中的潜力，结果超乎预期。在有限的人类高层指导下，Claude 于 11 天内完成端到端形式化证明。
初期多 Agent 直接协作曾导致进度混乱。关键转折点在于彭天翼团队打造的 Prove2Me 数学形式化协作平台。
Prove2Me 将庞大证明拆解为有向无环图（DAG），顶层为费马大定理，下层为不断细分的中间定理。不同 Agent 分别负责定义概念、证明引理或利用既有结果向上推进，并可搜索复用已完成结论。
最终，Claude 生成约 30300 个可验证定理，其中 29500 个纳入最终证明，代码总量约 1300 万行。结果通过 Lean 完整检查，仅使用三条最基础标准公理。
▲克劳德・怀尔斯 (Claude Wiles) 用 Prove2Me 计划形式化费马大定理的关键里程碑。图中三个彩色部分分别对应克劳德在最终目标实现过程中必须证明的三个核心子定理。该图与怀尔斯最初的证明过程非常吻合。
研究团队通过比较程序确认，Claude 最终证明的数学命题与 Mathlib 中费马大定理的正式定义完全一致。
03. 带队大神，出自清华姚班
项目负责人彭天翼履历亮眼。其本科毕业于清华大学姚班，曾获信息学奥赛国家集训队资格及清华大学优秀毕业论文奖。
▲彭天翼
2017 年，彭天翼赴麻省理工学院深造，2023 年获博士学位。研究方向从量子信息逐渐转向大规模决策系统、强化学习及因果推断。
2023 年前后，他参与创立 Cimulate.AI，搭建基于 Transformer 和强化学习的电商搜索系统 CommerceGPT。目前，作为哥伦比亚大学商学院助理教授及 Anthropic 研究员，他长期带领团队主攻强化学习、AI 智能体及形式化工具研发。
04. 结语：AI，正在加速改变数学研究的模式
Claude 此次突破并非解决未攻克猜想或取代人类证明，而是首次将跨多领域的庞大证明工程完整推进至机器可验证阶段。
AI 在数学领域的角色已从解题延伸至知识整理、证明转写和结果验证等基础科研流程。
过去，形式化证明因依赖人工、周期长而难以普及。如今，大模型、多 Agent 协作与 Lean 系统的结合，正推动大规模自动形式化从耗时工程向可规模化复制的科研基础设施演进。
智东西