🎯 科技 · AI突破

11天完成350年数学工程，Claude改写人类形式化证明的历史纪录

一、11天完成350年难题，Anthropic放王炸

9月4日，Anthropic宣布了一项震撼数学界和AI圈的消息：Claude在人类少量指导下，用11天完成了费马大定理的完整形式化证明。这项工程由清华姚班校友、哥伦比亚大学助理教授彭天翼（Tianyi Peng）发起，成果已公开在GitHub上。

费马大定理是数学史上最著名的难题之一：当整数n大于2时，不存在满足aⁿ+bⁿ=cⁿ的正整数a、b、c。费马1637年在书页边缘写下这个断言，声称找到了"绝妙的证明"，但页边太窄写不下。此后350多年，一代代数学家前赴后继，直到1995年怀尔斯和泰勒才完成完整证明，长达129页。

而这次Claude完成的，不是发现新证明，而是把怀尔斯的129页证明及其所有依赖的数学知识，全部转写成计算机可以逐步核验的Lean代码。整个过程生成了约1300万行Lean代码、2.95万个中间定理，消耗约60亿输出token。

二、1300万行代码，是Mathlib自身规模的5倍

这个体量有多夸张？Lean核心数学库Mathlib是人类数十年积累的精华，而Claude这次产出的代码量是其5倍以上。数十个Claude智能体同时参与，分工明确：有的负责补数学定义，有的专门攻中间引理，有的沿着已有成果往更高层定理推进，还有的负责把不同部分重新拼回整个证明体系。

项目并非一帆风顺。早期多Agent协作很快撞上了"人一多就乱"的经典难题——Agent们逐渐跟不上整个项目的状态，协作效率急剧下降。失败尝试留下的代码最终只占成品非模板代码的约7%。转折点在于换上了彭天翼团队专门为数学形式化搭建的协作平台"Prove2Me"，它将证明拆成有向无环图，每个Agent都能从全局视角判断下一步该攻哪个定理节点。

三、AI时代，谁来为数学证明背书？

费马大定理早已得到公认证明，为什么要做形式化？这背后是一个越来越紧迫的问题：当AI生成的数学证明越来越多，谁来确认它们是对的？

传统数学论文的写作方式是面向同行，省略显而易见的步骤，直接引用前人结论。审稿人核查一项复杂结果时，需要沿着引用和推导追溯很长的逻辑链条，往往持续数月甚至数年。Lean等证明助手采用"命题即类型"的设计，将每一步推理转化为代码，由计算机严格检查。即使生成证明的模型经常出错，只要检查环节可靠，就能确保最终结论无误。

清华大学求真书院此前也推出了FormaTheoria系统，辅助形式化"有限单群分类"这一近两万页的超级证明工程，目前已产出99.4万行代码。彭天翼的Claude费马大定理项目证明了一条可行路径：人类负责确定问题方向，AI承担大规模推导，形式系统确保每一步可验证。这或许就是AI时代数学研究的新范式。

综合DeepTech深科技、量子位、机器之心、网易新闻、清华大学官网报道 | 2026年9月6日