有限单群分类定理大概是史上最长的证明：500 多篇论文、约 15000 页、约 100 位数学家。Axiom Math 用几十个 AI agent 跑了 24 天，把它翻成了 4310 万行 Lean 代码，205 万条声明，100 个里程碑。

先纠两个被二传放大的数：AINews 写「约 5000 万行」「数百处勘误」，官方是 43.1M 行、34 处偏差，Axiom 自己说「数百处」是夸大。

最大的一处来自 Walter 1986 年的论证，反例是 PSL2(49)；改走 Solomon 1976 路线修补，还产出了新定理。

边界：Lean 只验证推导，不验证陈述本身，且只覆盖单向。这不是「数学被机器证明了」。