Axiom Math完成有限单群分类定理首个完整Lean形式化证明，24天产出4310万行可验证代码

SmartHey10月29日消息，北京时间10月26日，AI数学研究机构Axiom Math宣布重大突破：依托数十个AI智能体协同工作，仅用24天即完成有限单群分类定理（CFSG）的全链条Lean形式化证明，生成约4310万行可被计算机逐行验证的代码。这是该定理自20世纪问世以来，首套经机器内核严格校验、逻辑闭环完整的证明版本。

有限单群分类定理被誉为二十世纪数学最宏大的成就之一，素有“巨大定理”（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构造出明确反例，证伪Walter 1986年回忆录中一条关键闭包断言。该反例虽未否定定理结论本身，却宣告原有推导路径失效。

Axiom团队联合群论泰斗Richard Lyons与Ronald M. Solomon，基于Solomon早年的2-极大分支理论，不仅重构了UGT的完整证明，更进一步提炼出全新定理——“单顶保持定理”，成功打通整个分类体系的关键逻辑链路。

团队还另寻到一条适配第一代证明框架的更简捷推导路径，两套方案均已纳入配套学术论文。此外，AI还发现Aschbacher‑Smith拟薄群专著中某引理存在等式错误；研究人员通过将等式修正为不等式，并重新划分案例完成修复，确保整条证明链严丝合缝。

正如数学家Aschbacher所言：“撰写超长复杂论证而完全不出错，几乎是不可能的。” 形式化证明的价值，不在于质疑前辈，而在于将跨越数十年的分散推理凝练为可固定、可追溯、可复现的数字知识体，将潜藏于文献中的缝隙显性化，并提供经验证的修补范式。

Axiom团队强调：有限单群分类定理的数学本质，仍是上百位群论学者集体智慧的结晶；Axiom的核心贡献在于实现机器可校验落地、系统定位文献瑕疵，并交付一条完整、稳固、开放的证明链路。项目将全面公开勘误总表、全量代码仓库、依赖关系图谱，以及不平衡群定理修复专题论文，供全球代数学家与数学物理研究者自由调用。未来，团队还将联合领域专家顾问委员会持续维护与更新这份巨型数学知识库。

当前，代数、数论、组合学及理论物理领域的大量研究直接引用CFSG，却常因证明过于庞杂而省略细节。这一首个完整机器核验版本，将使后续科研工作者得以精准回溯每一条推论的前提、依赖与边界条件，为AI深度赋能前沿数学研究树立全新范式标杆。