15,000页数学证明，AI swarm 24天验证完毕，顺手揪出2000多个错误

10月27日，Axiom宣布完成有限单群分类定理（CFSG）的Lean形式化验证。这是数学史上最长的证明：约15,000页，由100多位数学家历经30年写成，此前没有任何一个人通读过。

一群AI智能体在24天内完成了验证。它们自己分工、认领任务、互相审查，像工程团队一样在GitHub上协作。最终每一步都被Lean内核检查过——结论不依赖对AI的信任，而是被机器证明为正确。

这个项目产生了4310万行Lean代码，是迄今最大的Lean代码库。过程中，AI发现了2000多处人类遗漏的错误，其中34处构成实质性偏差。

CFSG试图列出所有有限单群——有限群的不可再分“原子”，相当于对称性的周期表。定理声称，每个有限单群要么属于素阶循环群、交错群、李型群这些无限族，要么是26个散在群之一，其中包括最大的散在群“怪兽”，它有大约8×10^53个元素。这个定理的证明散布在500多篇论文中，依赖关系极其复杂，所以一直有正确性疑云。

来源：S. D. Smith; ATLAS of Finite Group Representations.

时间线显示了从Galois到Axiom的历程：

Lean是一种证明助手语言，数学定义、陈述和证明可以精确到让计算机检查每一步。形式化就是把整个证明翻译成Lean代码，迫使每个逻辑缺口被补上。

Axiom为智能体提供了人工搭建的证明地图，将整个证明拆成108个里程碑和约380个任务。智能体认领任务、寻找相关论证、翻译成Lean，并可以委托其他智能体准备前置条件。过程中出现很多问题：早期一些里程碑隐藏着巨大前提，团队删掉了上万行建立在错误假设上的代码重新来过。工程师还开发了分布式缓存和并行检查，避免构建时间成为瓶颈。

10月10日，一条消息出现在频道：“我们证明了Monster是单群。”智能体还通过Griess代数正式化了Monster的存在，并证明了一个识别“Monster型”群与Monster同构的定理。

里程碑完成进度：

最有意思的发现发生在非平衡群定理（UGT）上。这个定理帮助从子群信息识别整个群。Axiom试图形式化John Walter 1986年的证明，结果智能体找到了明确的反例：一个闭包断言假设某个操作会将相关单群保持在一个族中，但操作可能产生被排除的群。比如从PSL₂(49)出发，其域对合的中心化子包含PSL₂(7)，而7是梅森素数，被排除在族外。

换句话说，沃尔特的论证有一个真实漏洞。但反例没有推翻UGT本身。Axiom与Richard Lyons和Ronald Solomon（CFSG的主要贡献者）协商，基于Solomon 1976年的极大2-分量理论，让智能体证明了一个新结果（定理2.3“简单顶的保持”），替代了原有步骤。这个新结果也构成了UGT论文的核心。

Aschbacher在2005年写道：“写一个很长很复杂的论证而不出错是不可能的。”这次形式化把这句话变成了具体案例。

这对软件工程意味着什么？目前编码智能体可以写大量代码，但每一行仍需人类审查。如果一群智能体能协调处理4000万行数学证明并证明每一步正确，同样的方法可以应用于软件。整个代码库由智能体编写、检查和交付，无需人类抓bug——这正是Axiom下一步的方向。

有网友评论：“自检查的部分很疯狂。想象把这种验证水平应用到生产代码。”另一位说：“有趣的不只是抓到2000个错误，而是检查与编写是分开的。代码也一样：写PR的智能体不应该是审批它的那个。”

完整的证明地图和代码已在GitHub公开，Axiom邀请群论学家和Lean社区重新运行验证。这是数学史上第一次，超过100位数学家的工作被完整地机器检查。无论你对AI形式化数学持什么态度，一个事实已经无法忽略：人类没读过的证明，AI读了，而且读得很认真。