数学史上最长的证明，被一群 AI 智能体在 24 天里过了一遍。有限单群分类定理（CFSG）横跨 500 多篇论文、约 15,000 页，是公认没人能完整读完的巨兽。Axiom 把它转写成 3800 万行以上的机器验证代码，顺手在已发表文献里挖出 34 处严重出入。
这 34 处才是重点。CFSG 自上世纪八十年代被宣布完成以来，一直靠着研究者的互相引用维持权威，局部勘误不断，却从未有过一次彻底的、可由机器复算的检验。人类数学里最庞大的一个结论，几十年来建立在"大家相信它是对的"之上。形式化验证把这个前提掀开了一角——不是推翻定理，而是告诉你地基里究竟哪几块砖是歪的。对于任何依赖 CFSG 的下游工作，这都不是小事。
更值得盯的是曲线的斜率。公开数据显示 Axiom 的 CFSG 形式化代码已达 43.0M 行，大约每 37 天翻一倍，规模可能已经挤进最大的开源项目之列。这条增长曲线说明的不是"AI 会做题了"，而是 AI 开始承担学术基础设施里最枯燥、最不讨好、也最没人愿意干的那部分工作：逐行核对。数学界的下一场争论，很可能不再是某个证明对不对，而是谁的代码库更可信。
