据10月28日的报道，Axiom公司宣布，它用计算机验证了“有限单群分类”——这是数学史上最庞大的成果之一，原始证明横跨数百篇论文、总计约15000页。Axiom的Lean形式化成果约有4310万行，AI智能体在其中协助完成了大量工作，整个过程据称只用了24天。Lean会逐行检查每一个逻辑步骤，但数学家仍然需要确认：形式化写下来的命题，是不是真的是原来那个数学命题。这个提醒，恰恰是这件事最有价值的部分。
15000页，到底难在哪里
有限单群分类不是一道题，而是一座城。它由几代数学家接力完成，证明分散在不同年代、不同作者、不同记号体系的论文里，中间还有过“证明有缺口、后来补上”的插曲。人类读完它都很难，更别说确认每一处推理都没有跳步。形式化的意义，就是把这座城的每一块砖都编号、称重、重新砌一遍：任何一处逻辑断裂，机器都会立刻指出。这不是“AI比数学家聪明”，而是“机器比人类更适合做永不疲倦的校对”。
24天这个数字，应该怎么理解
24天不等于“AI独自证明了分类定理”。它更准确的含义是：在已有数学成果和形式化工具的基础上，AI智能体大幅加速了“把已有证明翻译成机器可检查形式”的过程。这个翻译工作过去被认为是苦活、累活，没人愿意干，也很难拿到学术荣誉。AI的出现，恰恰是把这种“高价值但低荣誉”的苦活变成了可规模化的工程。一旦翻译完成，后人就可以在这个坚实的地基上继续往上盖，而不用每次都怀疑地基有没有裂缝。
真正的变革，可能不在数学，而在所有“长证明”学科
数学之外，物理、计算机科学、密码学里也有大量“很长、很难复核”的论证。如果形式化+AI的模式跑通了，这些学科的“可信度基础设施”都会升级：论文不再只靠同行凭经验点头，而是附带一份机器可检查的证据链。当然，这也带来新问题：形式化本身会不会出错？定义翻译会不会走样？这些都需要第二层、第三层的检查。科学的可信度，从来不是靠一个工具一次解决的，而是靠一层层互相制衡的检查堆出来的。
写在最后
4310万行代码和24天，最打动人的不是速度，而是态度：人类最宏大的智力成果，终于有了一份机器也能逐行读懂的版本。AI没有取代数学家，它只是让数学家第一次可以说——这座15000页的大厦，我不仅相信它是对的，我还能指给你看，每一步为什么对。
