10月29日消息，北京时间 10 月 26 日，AI 数学研究机构 Axiom Math 对外发布重磅成果：借助数十个 AI 智能体集群，仅耗时 24 天，完成有限单群分类定理（CFSG）的完整 Lean 形式化证明，产出约 4310 万行可被计算机逐行校验的代码，这也是该定理问世以来，第一套完整经过机器内核核验的证明版本。

有限单群分类定理被誉为二十世纪数学最重要成就之一，也被称作巨大定理（Enormous Theorem），是描述有限对称结构的 “元素周期表”。

原始证明散落于 500 余篇学术论文，累计约 15000 页，前后有近百位数学家接力数十年才完成，整套文献体量庞大，没有任何一位学者完整通读全部证明材料，人工全面校验几乎不可能实现。

该定理把全部有限单群划分为四大类别：素数阶循环群、阶数大于等于 5 的交错群、16 类李型无穷群，外加 26 个孤立的散在群，其中就包含著名的魔群（Monster group），魔群拥有约 8×10⁵³ 个元素，是体量最大的散在有限单群，在模形式、黑洞熵、弦理论等数学物理方向均有重要应用。

历史上这套证明也历经多次补全修正。1983 年数学家 Gorenstein 宣布证明完工，但后续发现拟薄群案例存在关键手稿缺口；直到 2004 年，Aschbacher 与 Smith 以 1221 页专著补齐该漏洞，形成所谓 “第一代证明”；学界同时推进结构更简洁的第二代重写版本，但截至目前尚未全部完稿。因此 Axiom 本次形式化工作选择以成熟的第一代证明为蓝本开展工作。

本次项目中，研究团队搭建了完整 “证明地图”，将庞大的证明拆解成 108 个里程碑、380 个子任务，交由 AI 智能体集群分工完成：部分智能体拆解复杂命题、开展评审，部分智能体检索已有数学结论，将纸质文献的逻辑翻译为 Lean 形式代码；人类数学家负责处理数学障碍，工程师优化分布式缓存系统，解决千万行代码带来的编译、重复校验性能瓶颈，实现大规模并行验证。项目也复用了 Mathlib 数学库以及 Qiuzhen‑CFSG 项目约 120 万行已有成果，站在社区前人工作基础之上推进开发。

将纸质数学论证转为机器可理解的形式化代码的过程中，计算机不允许任何默认省略、隐性假设，迫使所有逻辑环节显式呈现。项目团队累计发现34 处值得关注的文献偏差，多数为笔误、表格错误、条件遗漏；其中最重大一处漏洞来自不平衡群定理（UGT）的旧版证明：AI 找出明确反例，指出 Walter1986 年回忆录中一条闭包断言并不成立，但该反例并未推翻不平衡群定理本身结论，只是原有推导路径失效。

Axiom 团队联合该领域元老级数学家 Richard Lyons、罗纳德·索洛蒙（Ronald M. Solomon），基于索洛蒙早年 2‑极大分支理论，不仅重构了不平衡群定理的完整论证，还产出一项全新群论结论 ——“单顶保持定理”，以此打通整个分类证明的关键链路。

后续团队还找到了一条适配第一代证明体系的更简短推导路径，两套方案均被写入配套学术论文。除此之外，AI 还发现 Aschbacher‑Smith 拟薄群著作内一条引理的等式错误，研究人员通过把等式修改为不等式、重新划分案例，完成修复，保证证明链条闭环。

“撰写超长复杂论证，完全不出错几乎是不可能的。” 数学家 Aschbacher 曾这样评价巨大定理。形式化证明的价值不在于否定前辈数学家的成果，而是把分散数十年的推理链条完整固定下来，把文献中潜藏的缺口显性化，并且给出可复现、可复查的修复方案。

Axiom 团队强调，有限单群分类定理本身的数学结论依旧是上百位群论学者的集体智慧结晶；Axiom 的贡献是完成机器可校验实现、定位文献瑕疵，并且提供修补后的完整证明链路。项目会对外公开勘误总表、完整代码仓库、依赖关系图谱以及不平衡群定理修复专题论文，供全球代数学家、数学物理研究者使用。未来团队还将联合领域专家顾问委员会持续维护勘误清单，持续完善这份巨型数学知识库。

代数、数论、组合学与理论物理大量论文会直接引用有限单群分类定理，但很多作者并不会展开复述其复杂证明。这套完整机器核验版本，将让后续科研工作者可以精确追踪每一条推论背后的前提条件与依赖关系，为 AI 辅助现代前沿数学研究树立新的范式标杆。