数学 AI 公司 Axiom 宣布，它的 AxiomProver 智能体集群在 24 天里完成了有限单群分类定理（CFSG）的 Lean 形式化，称这是这条定理第一份完整的计算机检查证明。代码已在 GitHub 以 Apache-2.0 许可证开源，仓库声明最终版本里没有 sorry 占位、没有用 native_decide，只依赖命题外延性、经典选择公理和商的可靠性三条标准公理。
有限单群分类常被叫作”对称性的元素周期表”。它说明所有有限单群要么属于 18 个无限族，要么是 26 个散在群之一。原始证明分布在 500 多篇论文里，约 1.5 万页，由大约 100 位数学家从 1955 年前后写到 2004 年，最后一块 quasithin 部分出自 Aschbacher 与 Smith，单篇就有 1221 页。
24 天里发生了什么
按 Axiom 公布的过程，项目 10 月 1 日建了 Slack 协作群，10 月 2 日第一批智能体上线。整份证明被拆成 108 个里程碑、约 380 个小任务，智能体在 GitHub issue 上认领任务、在 Slack 里汇报进度。主导智能体负责拆题和审查命题，其余智能体检索已有结果或编写 Lean 证明，缺前提时再往下派活。
过程并不顺。早期一批代码因为隐含假设出错被整片删掉，团队重新规划；后来构建速度成了瓶颈，工程师用缓存、并行检查，把有限计算外置成可验证的证书，完整构建时间压到 24 小时以内。10 月 10 日，项目先单独宣布证出 Monster 群是单群。
语料方面，Axiom 称一共读入 715 篇论文和书籍，并复用了此前 Qiuzhen-CFSG 项目约 120 万行代码，还有 Mathlib、Tau Ceti 等既有形式化库。
顺带挑出的错
形式化过程中，团队记录了 34 处较明显的数学偏差。最受关注的一处在”不平衡群定理”（UGT）路线上：Walter 1986 年回忆录中的一个闭包断言有反例，从 PSL₂(49) 出发会推到 PSL₂(7)，而后者恰好被该族排除在外。Aschbacher–Smith 的一条引理也找到了 SL₂(5) 反例，等式改成不等式后，后面的论证要跟着扩展。
Axiom 为此单独发了一篇 35 页的论文，提出替代论证，并在 Lyons、Solomon 等顾问参与下修补这条路线。公司反复强调，这些反例没有推翻 UGT 本身，更没有动摇分类定理。
“the classification remains the achievement of the mathematicians who discovered the groups” （分类仍是发现这些群的数学家们的成就。）
跟以往的机器验证比
横向看，最常被拿来对照的是 Gonthier 团队 2012 年在 Coq 里完成的奇数阶定理验证。那条定理源自 Feit 与 Thompson 1963 年 255 页的论文，项目前后约六年，是分类证明里的一块基石。Axiom 这次覆盖的是整座大楼，用时按天计。
两者不能直接比速度。奇数阶项目当年几乎从零搭库，Axiom 站在 Mathlib 和先前 120 万行 CFSG 代码之上，智能体数量是”数十个”，背后的算力、硬件和总成本都没有披露，人时数也没公开。24 天是形式化项目本身的周期，不包括它所依赖的几十年人类工作。
几处保留意见也写在明处。项目元数据把审查标注为”自我评估”，目前还没有第三方从干净环境复现完整构建；机器检查只能保证推导从写下的假设出发成立，分类陈述的定义是否忠实于原定理，仍要群论学者逐条核对。那篇 UGT 论文发在不做同行评审的预印本平台上，勘误表 Axiom 说会挂在项目页面。
对做形式化的人来说，下一步看两件事：社区能否独立跑通这 4310 万行，以及 34 处偏差里有多少能被原作者一方确认。
参考来源：Axiom 项目公告与 GitHub 仓库、Unite.AI、CocoLoop、Kingy AI；Lean 代码行数、声明数、里程碑数与偏差数以 Axiom 公布口径为准，奇数阶定理验证周期据微软研究院资料。