Axiom团队24天完成有限单群分类定理形式化，4310万行Lean代码刷新开源项目纪录

2026年10月27日，美国AI数学初创公司Axiom宣布：人类数学史上篇幅最长的证明——有限单群分类定理（Classification of Finite Simple Groups, CFSG），已完成全链条形式化验证。整个过程由其自主研发的多智能体系统AxiomProver执行，仅用24天便生成4310万行Lean代码，构建出迄今规模最大的开源软件项目。该成果已全部开源至GitHub，标志着数学证明的可信性验证迈入新阶段。

这一成就的核心在于“形式化”——即将自然语言书写的数学证明逐句翻译为计算机可严格校验的形式语言。在Lean等证明助手中，“显然”“同理可得”等模糊表述不再被接受，每一步推理、每一个隐含前提都必须显式写出并经内核验证。这不仅提升了证明的严谨性，也为AI参与高阶数学研究提供了可信赖的接口。

有限单群分类定理被誉为数学界的“对称性周期表”。它断言：所有有限单群（即无法进一步分解的对称性基本单元）仅有四类——素数阶循环群、交错群、16个李型群家族，以及26个无法归入上述类别的“散在群”。其中最大的“魔群”（Monster Group）包含约8×10⁵³个元素，其结构之复杂曾长期超出人类直觉范围。该定理的原始证明始于20世纪50年代，由约100位数学家历时数十年、发表500余篇论文、累计约15000页内容完成，相当于14部《红楼梦》的篇幅。由于证明极度分散且依赖大量交叉引用，1983年Gorenstein宣布完成时，实际仍存在重大缺口；直至2004年，Aschbacher与Smith才以1221页专著补上“拟薄群”情形的关键部分。

正因如此，CFSG长期被视为“无人能通读”的“巨型定理”。即便在第二代系统性重写计划启动后（截至2023年已出版10卷，预计共12卷），其完整性与可验证性仍面临挑战。而Axiom的突破在于：将整套证明拆解为108个里程碑与约380项子任务，交由数十个AI智能体协同推进。这些智能体分工明确——有的负责解析高难度论证，有的检索已有结果，有的编写Lean代码；当某环节缺失前置引理时，系统会自动派发新任务。整个流程高度自动化，但也带来工程挑战：AI产出速度过快，导致Lean依赖检查频繁触发算力瓶颈，团队不得不紧急开发分布式缓存系统以维持进度。

值得注意的是，AI不仅复现了人类证明，还主动发现了原证明中的疏漏。在形式化过程中，系统识别出Unbalanced Group Theorem相关推导存在逻辑断层，并自主构造新引理完成修补，最终实现完整闭环。这意味着AI已从“翻译者”升级为“协作者”，具备独立发现与修正能力。

该项目的规模令人震撼：4310万行Lean代码远超Linux内核（约2800万行）、Chromium（约2500万行）、Firefox（约600万行）等知名开源项目，成为当前全球最大开源代码库。其结构清晰标注了各模块来源——涵盖经典群、李型群、散在群等类别，每部分均对应具体论文或书籍依据。Axiom强调，所有代码与证明地图均开放访问，支持任何人复现、审查或在此基础上继续扩展。

在技术路径上，Axiom并未采用单一超大模型暴力生成，而是构建了“人机协同+多智能体调度”的混合架构。人类专家负责定义任务边界与验证关键节点，AI则承担重复性高、逻辑严密的编码与推导工作。这种模式既规避了纯端到端生成易出错的风险，又充分发挥了AI在规模处理上的优势。据公开信息，团队由00后创始人领衔，核心成员兼具数学与计算机背景，成立仅一年半即达成此项里程碑。

此举也引发学界对数学研究范式的深层讨论。传统上，数学证明依赖同行评议与专家共识；如今，形式化验证提供了一种客观、可重复的替代路径。尤其在AI加速产出新证明的背景下（如OpenAI近期在调和分析、量子场论等领域发布数百份模型生成手稿），如何确保其正确性已成为紧迫问题。CFSG的形式化为此提供了可行范本：通过Lean这样的工具链，将“信任”从人际传递转向机器可证。

数学家Ken Ono在见证该成果时动情表示，这让他想起父亲——一位群论研究者——早年引领他接触这一领域的场景。当人机协作跨越半个世纪的鸿沟，抵达理论终点线时，他当场落泪。这一情绪反应背后，是几代数学家对“终极分类”梦想的集体投射。

目前，Axiom已将该项目命名为“CFSG Formalization Project”，并持续更新其Proof Map（证明地图），允许用户追踪任一结论的推导路径。团队透露，下一步将聚焦于更复杂的数学对象，如代数簇分类与朗兰兹纲领的部分命题。与此同时，多个高校与研究机构已开始基于该代码库开展教学与验证实验。

形式化并非取代数学直觉，而是为其提供坚固的地基。当4310万行代码在服务器中静静运行，每一次Lean内核的“✅ Verified”反馈，都在重申一个事实：最抽象的思维成果，终可被最精确的机器所确认。