Anthropic：Claude用11天完成费马大定理首个端到端形式化证明
约1300万行Lean代码、3万个中间定理，规模超Mathlib五倍；多Agent协作一度失败，靠Prove2Me平台加Claude Code harness完成全流程。
AI解读：这条新闻的关键不是AI又攻克了一道数学难题，而在于它把数学界原本打算用多年社区工程来做的“形式化”工作压缩到了11天。数学家看普通论文时能脑补“这里显然成立”，但Lean系统要求每一步推导都从公理出发、逐行可查，这正是人力形式化大定理耗时极久的原因——帝国理工的Kevin Buzzard团队2024年才刚启动这类项目，蓝图就有86页。Claude这次的角色是“翻译”：把人类可读的Wiles证明改写为约1300万行Lean代码，中间约3万个定理，经Lean三个标准公理检查通过，且它与Mathlib中的定理陈述已被比对一致。对直接受影响的人来说，意义在于数学文献的形式化第一次有机会摆脱“手工作坊”模式——若这套流程可以复制，验证新论文、建立计算机可查的证明档案的成本会明显下降。但要冷静看待几个限制：Claude没有发明新证明，产出仍是Wiles的旧结论；过程中大量工作并非纯靠Claude单干，而是被拆给数十个并行的Agent，并依赖Anthropic研究员Tianyi Peng团队搭的Prove2Me分工系统来调“队形”；它也不是神速到底，早期多Agent协作失败留下的代码占成品非模板代码约7%，全靠最后换上的harness才拢住。这更像一次工程能力的演示，而非数学方法的突破。普通人不需要为此做任何准备，但关注科研自动化的人可以留意：同等规模的定理若能被这套流程复现，数学期刊的“核验”环节或许会从论文发表后数年的漫长等待变成一种常规操作。
Anthropic于2026年9月5日宣布，其AI Claude完成了费马大定理的首个端到端、可由计算机完整检查的形式化证明，用时约11天。据量子位报道，最终成果为约1300万行Lean代码、超过3万个中间定理，最终证明使用了其中约29500个，代码规模超过Lean核心数学库Mathlib的5倍。Anthropic称，完整证明只依赖Lean的三个标准公理，并通过比较程序确认Claude最终证明的定理陈述与Mathlib中的费马大定理完全一致。
证明背景与形式化任务
费马大定理指，对任意整数n>2，不存在正整数a、b、c使aⁿ+bⁿ=cⁿ。该命题由17世纪法国数学家皮埃尔·德·费马提出，历经欧拉、勒让德、库默尔等数学家推进，直到1993年英国数学家Andrew Wiles首次公开宣布证明，发现关键缺口后又与Richard Taylor用约一年时间修补，最终于1994年完成证明。
Anthropic强调，Claude并未发现新证明，而是把人类可读的Wiles证明“翻译”成计算机能逐行检查的形式化证明，即Lean代码。Lean是一种证明助手系统，要求每个数学推导步骤都明确从公理和已证定理推出，不接受“显然成立”等省略。
- Claude 11天完成形式化，产品与内外部项目耗时对比暂无更长周期数据；量子位报道指，2000年代已有计算机科学家提出形式化Wiles证明设想，2024年帝国理工学院Kevin Buzzard等人才正式启动多年社区项目，其第一阶段技术蓝图长达86页。
多Agent协作工具Prove2Me
Anthropic研究员Tianyi Peng是本次项目的负责人。据量子位报道，其2017年从清华大学姚班本科毕业，2023年获MIT博士学位，现任哥伦比亚大学助理教授、Anthropic研究员，方向为强化学习、AI Agent与形式化工具。Peng最初只是想测试Claude能把费马大定理形式化项目推进多远。
整个过程中，多个Agent被并行拉起：有的补数学定义，有的攻中间引理，有的沿已有成果向上推进，另有Agent负责把各部分拼回整个证明体系。但项目早期多Agent协作很快遇到问题——工程规模扩大后，Agent逐渐跟不上项目状态、协作效率下降，早期失败尝试留下的代码约占成品非模板代码的7%。
转折点是改用Tianyi Peng与其哥伦比亚大学合作者搭建的Prove2Me平台。该平台把证明拆成由定理节点组成的有向无环图（DAG），每个定理的证明状态、缺失前置条件、下一步攻击节点都能被Agent判断；平台还分离管理定理陈述与证明、加速Lean编译，并为每个定理保留自然语言描述，方便Agent搜索和复用。Anthropic最终使用的是Prove2Me，配合基于Claude Code的multi-agent harness。
- 项目总消耗约60亿个输出Token，内部使用的通用研究模型能力大致相当于Claude Fable 5.1（据Anthropic）。
- 人类在过程中提供的数学指导有限：Peng只在高层给出提示，如某个方向优先级更高、某个定理需尽快推进，大量定义、中间证明、任务拆分和拼装由Claude自主完成。
- 负责审阅结果的帝国理工教授Kevin Buzzard称其为“非凡的自动形式化成果”。量子位报道还推测，若如此规模和复杂度的现代数学成果可被AI自动形式化，过去依赖人工、推进缓慢的数学文献形式化可能具备大规模提速条件。