Claude完成费马大定理首个完整形式化证明，姚班校友主导、全程机器可查

量子位报道，Anthropic刚刚宣布，Claude已完成费马大定理的首个端到端、可由计算机完整检查的形式化证明——把人类数学家能读懂的证明，彻底翻译成计算机能一行一行核对、没有任何"这里显然"的形式化代码。困扰数学界350多年的命题，第一次以机器可逐行验证的完整形态被证明。

所谓形式化证明，是让定理、定义和每一步推理都以Lean证明助手能理解的形式写出，由Lean逐一验证每个推导是否合法地来自公理和先前定理。普通数学论文写给数学家看，许多步骤可以用一句"显然成立"带过；形式化证明则不允许任何跳步。据报道，此次证明的Lean代码规模约达1300万行。

费马大定理从17世纪费马写下命题起，历经欧拉、勒让德、库默尔等一代代数学家推进而始终未能完整攻克，直到1994年怀尔斯与Richard Taylor完成修补，才为这条横跨350多年的难题画上句号。而把整套证明搬进计算机可验证的体系是另一项浩大工程：2024年，帝国理工学院的Kevin Buzzard等人启动一个多年社区项目，计划用Lean完成费马大定理的形式化，仅第一阶段的技术蓝图就写了86页。

主导此次成果的是清华姚班校友Tianyi Peng：他2017年从姚班本科毕业、2023年获MIT博士学位，如今是哥伦比亚大学助理教授、Anthropic研究员，长期聚焦强化学习、AI Agent与形式化工具。项目采用多Agent分工——有的负责补齐数学定义，有的专攻中间引理，有的沿着已有成果向更高层定理推进，还有Agent负责把不同部分重新拼回完整的证明体系。

不过协作并非一帆风顺。Anthropic透露，早期Agent虽然很快拿下了一些结果，但随着工程规模扩大，它们逐渐跟不上整个项目的状态，协作也越来越困难。为此，Tianyi Peng与哥伦比亚大学合作者搭建了一套面向数学形式化的协作系统：哪个定理已经证明、哪个还缺前置条件、下一步该攻哪个节点，Agent都能从一张协作图中判断；平台还把定理陈述与证明分开管理、加速Lean编译，并为每个定理保留自然语言描述，方便不同Agent搜索和复用已有结果。

报道称，Anthropic最终使用的是Prove2Me+——一个基于Claude Code的multi-agent harness。整个项目消耗约60亿个输出Token，内部使用的通用研究模型能力大致相当于Claude Fable 5.1。Anthropic还表示，完整证明只依赖Lean的三个标准公理，并且他们专门通过比较程序确认，Claude最终证明的定理陈述与Mathlib里的费马大定理完全一致。

人类在其中的角色明显后撤：Tianyi Peng只是偶尔给出一些非常高层级的提示，比如哪个方向优先级更高、哪个定理要尽快推进。

这件事的意义在于，数学文献形式化长期是数学中最缓慢、最依赖人力的角落。当规模如此之大、依赖如此复杂的现代数学成果都能被AI自动搬进形式化系统，过去极度依赖人工、推进缓慢的数学文献形式化，可能第一次真正具备大规模提速的条件。接下来的看点，是这套多Agent协作与验证模式能否复用到其他大定理，乃至对可靠性要求更高的软件与安全验证场景。