Axiom 在有限单群分类形式化过程中找到局部论断反例

Axiom 团队在使用 Lean 系统对有限单群分类定理开展完整形式化验证时，成功发现原证明文本里两处中间引理存在明确反例，本次发现只针对证明过程中的局部推导步骤，有限单群分类定理本身的最终结论完全成立，没有受到任何动摇，团队随后完成了对应步骤的论证修补，给出全新替代推导方案，顺利完成总计 4310 万行代码的全流程机器核验，为这份长达 15000 页的经典数学证明补上严谨的计算机校验版本，进一步夯实了整个有限单群分类体系的逻辑可靠性。

一、本次反例发现的基础背景

1. 项目整体概况 有限单群分类定理被称为 “巨大定理”，由百余位数学家历经数十年完成，全部证明分散在五百多篇论文中，整体篇幅达到 15000 页，人工通读全本几乎无法实现。Axiom 团队依靠多智能体 AI 工具，在 24 天内把整套证明翻译成 Lean 形式化代码，逐行完成逻辑核验，在自动化推导中捕捉到人工审稿难以发现的局部漏洞。
2. 两处核心反例的出处 第一处来自 Aschbacher 与 Smith 的拟薄群研究文稿，一条引理认定两个数值严格相等，Axiom 给出 SL₂(5) 作为反例，两组数值分别为 1 和 2，等式并不成立；第二处来自不平衡群定理（UGT）的 1986 版证明，其中一条闭包断言存在漏洞，PSL₂(49) 构成有效反例，变换后得到的群超出了预设集合范围。
3. 问题边界说明 两处反例仅仅推翻了证明里的中间推导条件，并没有推翻不平衡群定理，更不会动摇整个有限单群分类的最终结论，只是原证明选用的论证路径存在局部瑕疵，更换论证路线就可以把逻辑补全。

二、发现反例的完整执行步骤

步骤 1：搭建形式化验证环境

团队选用 Lean 4.26.0 版本，依托 Mathlib 数学库搭建群论推导环境，把自然语言写成的群论论文逐条拆解为机器可识别的形式化语句，严格补齐所有前提条件，杜绝 “显然成立” 这类省略写法。

步骤 2：分模块逐段自动化核验

把整个有限单群分类证明拆分成数百个子模块，优先核验不平衡群定理、拟薄群定理等高难度章节；AI 智能体自动执行每一步逻辑推演，一旦出现推导矛盾，立刻自动检索有限群实例，生成具体反例。

步骤 3：定位漏洞并生成反例

当程序在闭包断言与数值等式两处出现推导失败时，系统自动遍历有限群样本，先后输出 SL₂(5)、PSL₂(49) 两个具体群实例，精准验证该步骤条件不成立。

步骤 4：联合数学家修补论证

团队联络当年参与分类工作的资深群论专家，参考已有成熟论证思路，重新设计不含错误等式与闭包条件的推导路径，把修补后的证明再次录入 Lean 系统，完成新一轮全流程核验，消除全部逻辑缺口。

三、本次验证工作取得的成果

1. 完成全量形式化工程，产出 4310 万行 Lean 代码，实现人类最长数学证明的计算机全量核验。
2. 累计排查出 34 处值得重点修正的论证偏差，其余数百处均为文字笔误、表格数值写错、前提条件遗漏这类文书类问题。
3. 针对两处带反例的引理，给出严谨的替代证明，形成 35 页正式修订文稿，完善不平衡群定理的推导版本。
4. 建立起超长数学证明的 AI 形式化流水线，把过去数年才能完成的核验工作压缩到 24 天，大幅提升大型数学证明的校验效率。

四、后续技术优化方向

• 持续扩充有限群实例库，让 AI 能够更快生成反例，自动定位推导断点。
• 优化自动改写算法，在发现漏洞后自主生成多条备选论证路线，减少人工介入成本。
• 逐步把更多经典群论长篇证明纳入形式化核验范围，持续完善有限群论的机器验证体系。

【相关 FAQ】

问题 1：Axiom 在有限单群分类形式化里找到反例，会不会推翻有限单群分类定理？

回答 1：不会推翻有限单群分类定理。本次找到的反例只针对证明过程中的局部引理与中间断言，定理最终结论保持不变，只需要更换局部论证路径就能补齐逻辑，整个分类清单依然完全有效。

问题 2：Axiom 在有限单群分类形式化过程中找到的两处反例，分别对应哪两个有限群？

回答 2：第一处反例对应 SL₂(5)，用来推翻拟薄群文稿里的数值相等引理；第二处反例对应 PSL₂(49)，用来指出不平衡群定理闭包断言存在漏洞，两个群都可以直接在 Lean 环境里完成验算。

问题 3：Axiom 完成有限单群分类形式化并发现反例，采用的是什么验证工具与技术方案？

回答 3：项目采用 Lean 4 证明助手，搭配 Mathlib 数学库，依靠多智能体 AI 把 15000 页论文转写成形式化代码，自动逐行推演，出现矛盾时自动检索有限群实例生成反例，之后再重新编写修正后的证明语句。

问题 4：在有限单群分类形式化项目里，除了两处带反例的漏洞，Axiom 还排查出多少处其他问题？

回答 4：项目一共排查出 34 处重点论证偏差，除此之外还发现数百处文字笔误、表格数值错误、前提条件缺失等文书类小问题，全部都可以通过文字修订与补齐条件完成修正。

【数据来源】

[2026-10-28]（Axiom 报告有限单群分类形式化中发现反例）InfoQ

[2026-10-27]（Axiom 完成有限单群分类 Lean 形式化并修正论证漏洞）Unite.AI

[2026-10-26]（Formalizing the Enormous Theorem）Axiom Math 官方研究博客

[2026-10-26]（AI 完成巨大定理形式化，发现两处局部反例）微博学术博主马少平 THU

[2026-10-26]（有限单群分类证明中的反例与修补方案）XenoSpectrum 科技专栏

免责声明：本文全部内容来自 Axiom Math 官方公开研究文档、科技媒体公开报道；本次形式化项目的代码体量、反例细节、论证修补方案会随论文正式刊发小幅优化；文中技术成果仅为学术研究参考，不代表其他数学证明的通用校验结论。