一、从页边空白到机器可验证的一跃

1637年，费马在《算术》一书的页边写下那句著名断言：对任意大于2的整数n，方程a的n次方加b的n次方等于c的n次方不存在正整数解。他在旁边注明，自己发现了一个绝妙的证明，只是空白太小写不下。此后三百多年，无数数学家为此耗尽心血，仅1908年奖金设立后的第一年，就收到了621份错误证明。

1993年6月，Andrew Wiles在剑桥宣布证明，但随后被发现存在关键缺口，他与Richard Taylor又花了一年才补完，最终129页的证明于1995年正式发表。之后数学界又花了大量时间审阅：两位审稿人一度被迫重走整个论证过程。而这还只是人类可读层面的验证。

2026年8月18日凌晨，Anthropic的数十个Claude智能体在Prove2Me平台上读取到一个历史性信号：FLT ROOT读取为PROVED。费马大定理的完整证明被形式化到了Lean证明助手中，全程仅用11天，产出1300万行Lean代码，成为人类历史上最大的机器验证证明。

二、形式化证明与Lean：为什么琐碎步骤必须逐行写

形式化证明是把数学家脑中的推理链，逐条翻译成计算机可以自动检查的逻辑语言。它不依赖“显而易见”这样的省略，Lean内核要求每一步推导都显式可见。数学史上有大量教训：Wiles证明的审稿耗时一年；Hales的Kepler猜想让12人评审组花了4年，最终只敢说99%确定；Perelman的庞加莱猜想被社区接受用了约4年；Helfgott的弱哥德巴赫猜想至今仍在审查中。

Lean 4基于依赖类型论，把“命题即类型、证明即程序”的Curry-Howard对应变成工程现实：一个数学命题就是一个目标类型，一条证明就是构造该类型的程序，Lean内核用极小规模的核心逻辑完成验证，结论的真实性只取决于内核本身是否健全。这正是本文证明最硬核之处：最终产物只依赖Lean的三个标准公理propext、Classical.choice与Quot.sound，没有使用任何sorry、自定义axiom或native_decide逃逸通道。

三、Prove2Me：多智能体协作平台的设计

这个项目最关键的不是模型本身，而是协作架构。Tianyi Peng与哥伦比亚大学合作者设计的开源平台Prove2Me，用三个机制解决多智能体形式化数学的核心难题。

第一，定理陈述DAG。整个证明采用Darmon-Diamond-Taylor对Wiles证明的简化路线，被拆成有向无环图，每个节点是一条定理陈述，智能体按依赖关系决定下一步证什么，数十个智能体得以并行推进而不冲突。第二，陈述与证明文件分离：定理陈述和证明分存独立文件、链接单独维护，大幅加速Lean编译并最小化资源消耗，否则六万多个模块联合编译会瞬间压垮构建系统。第三，自然语言索引：每个定理陈述附带一段自然语言说明，智能体可以搜索并复用既有成果，寻找更短的证明路径。

有意思的细节是：智能体早期并非没有成果，但很快出现记忆退化——丢失项目状态、停止有效协作。切换到Prove2Me的DAG结构后才稳定产出；而早期失败尝试也并非全废，最终约7%的非样板代码行被保留进了终版证明。

四、规模与成本：1300万行、29500条定理、60亿token

来看这组工程数据：整个仓库包含60475个Lean模块，其中定义模块1450个、命题模块29511个、证明模块29511个，最终证明使用了约29500条中间定理，过程中共证明30300条。相比之下，Lean社区十年积累的主库Mathlib只有约250万行，这份证明的体积超过它五倍。60亿输出token按公开API价格折合约30万美元——而Kevin Buzzard领导、获得100万英镑资助的帝国理工社区项目，2024年启动时预期要花数年，仅蓝图就写了86页。

当然，规模大不代表漂亮。Buzzard在HN上回应说，Claude的证明很可能远长于必要长度，因为Mathlib是经过人类数百年雕琢的。这份证明大量借鉴了帝国理工FLT项目与flt-regular项目已有的106个文件，站在巨人肩膀上完成冲刺。人类输入极少：Tianyi只偶尔给出高层指令，比如推动Mazur定理尽快完成这样的战略调度。

五、双路验证：三公理约束下的独立内核复核

机器学习项目最怕看起来对。Anthropic为此设计了双路验证。第一路是leanprover/comparator：核验定理陈述与挑战文件一致、公理合规，并在完整环境里用Lean内核重放全部证明，耗时约15小时、峰值内存230GB，结论是解决方案正确。第二路更彻底：nanoda，一个用Rust独立实现的Lean内核，用37.8GB的导出环境重新检查了1052234个声明，零错误。两套内核互不共享实现，同时通过才可信。

此外，FinalCheck.lean把证明结果显式推导到Mathlib自身的FermatLastTheorem表述，从根上杜绝“证了个不一样的定理”。官方还发布了约390MB的离线静态网页与推理路线图，任何人都能逐条检查论证。整个证明以Apache 2.0协议开源。

六、意义：形式化数学的转折点

对数学界来说，AI形式化从玩具进入了核心定理级别：Frey曲线、Serre模性提升、Taylor-Wiles方法三大支柱全部机器验证。Buzzard的评价是：以不超出数学公理为前提证明了费马大定理，并认为这向现代数学文献的自动形式化迈出一大步，有望根除既有文献中的错误、减轻审稿人负担、严格检查LLM生成的数学。

对AI工程来说，Prove2Me验证了多智能体加可验证环境的组合拳：DAG分工解决长程任务的状态迷失，机器内核充当唯一裁判，模型只负责生成候选。Anthropic还做了一个小实验：三个个人版Claude Max订阅的智能体通过Prove2Me协作，3天就形式化了Vinogradov三素数定理——消费级订阅也能协作完成重大结果。

当然也有争议：有人质疑1300万行对129页论文来说过于臃肿，担心形式化成功变成堆算力的军备竞赛；Buzzard也提醒，自动形式化不等于自动理解，人类数学家对证明结构的洞察依然不可替代。但无论如何，2026年8月18日那个凌晨，数学正式进入机器仲裁时代。