Axiom Math用数十个Agent在24天内形式化有限单群分类定理

编辑｜Neo 100 多位顶尖数学家，耗费数十年，写下 1.5 万页证明。 现在，AI 只用了 24 天，就把这项人类数学史上最庞大的工程之一，变成了 4300 多万行可以由计算机逐步验证的代码。 更惊人的是，AI 在检查这些数学家留下的证明时，还揪出了一个存在近 40 年的论证漏洞。 这不是一道奥数题，也不是一篇几十页的数学论文，而是被称为「巨型定理」（Enormous Theorem）的有限单群分类定理。 从 20 世纪中叶开始，上百位数学家参与了这场研究。1983 年，数学家 Daniel Gorenstein 宣布分类工作已经完成，但此后人们发现其中仍有未补齐的部分。直到 2004 年，数学家又用 1221 页证明填上了一个关键缺口。 10 月 26 日，AI 数学公司 Axiom Math 宣布，由人类数学家和工程师组织的数十个 AI Agent，在 24 天内完成了这一巨型定理的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，给出了第一份覆盖整个分类定理的计算机检查证明。 原本分散在 500 多篇论文中的数学推理，如今被组织成一套能够逐步检查的形式系统。更让人意外的是，在这个过程中，Agent 不仅找出历史论文里的错误，还参与构造了一项新的群论结果。 Axiom 公开的有限单群分类定理形式化项目，包含约 4310 万行 Lean 代码、205 万个声明、100 个里程碑，涉及 715 篇参考文献。图源：Axiom Math 官网。 数学界花了数十年， 究竟在证明什么？ 理解这项工作的难度，要从「对称性」说起。 一张正方形纸片，旋转 90 度后，形状与原来完全重合；旋转 180 度、270 度也是如此。数学家把这些旋转操作及其组合构成的结构称为「群」。从几何图形到粒子物理，群论提供了一种研究对称性的通用语言。 复杂的有限群，可以在一定意义上分解为更基本的部分。就像整数能分解为质因数，这些不能继续拆分的「基本粒子」被称为有限单群。 有限单群分类定理要回答一个看似朴素的问题：所有这样的基本粒子，到底有哪些？ 最终清单包含素数阶循环群、交错群、16 个无穷系列的李型单群，以及 26 个特殊的「散在单群」。其中最大的「魔群」（Monster Group），拥有约 8×10^53 个元素。光是证明它存在，就曾是数学界的一项重大成就。 部分「散在单群」之间的关系示意图。其中，顶部的 M 代表最大的散在单群「魔群」（Monster Group），其他节点代表不同的散在单群。 找出这些群，只完成了一半工作。真正难的是证明：除了清单里的类型，不可能再有第 27 个散在单群，也不存在任何尚未发现的新类型。 1963 年，Walter Feit 和 John Thompson 用 255 页论文证明，所有非交换有限单群的阶都是偶数，为后续分类打开了突破口。1972 年，Gorenstein 提出 16 步研究计划；1983 年，他宣布分类完成。后来留下的拟薄群证明缺口直到 2004 年才由 Michael Aschbacher 和 Stephen Smith 补齐，2008 年又出现进一步修正。 庞大的证明像一张跨越数十年的关系网：某篇论文引用另一篇的定理，后者又依赖更早的引理。许多步骤还省略了作者认为显而易见的条件。即使每篇论文单独看起来合理，也很难由一个人检查整套体系的每一处连接。 Axiom 这次要做的，就是把这些连接全部转化成计算机能够核查的证明。 24 天的 Agent 工程， 差点被「正确的证明」拖垮 这不是让一个大模型读完 1.5 万页，再一次性吐出几千万行代码。 10 月 1 日，Axiom 开设专门的 Slack 频道，利用已有的 Lean 基础库和数学文献，整理出一张证明路线图：108 个里程碑、约 380 项具体任务。10 月 2 日，第一批 Agent 开始通过 GitHub Issues 认领任务。 有的 Agent 负责拆解定理，有的搜索已有结果，有的生成 Lean 证明，还有的审查命题、整合代码。遇到尚未完成的前置定理，Agent 可以继续将任务交给其他 Agent。人类数学家处理关键障碍，工程师则负责协调这些持续工作的系统。 这些 Agent 由 Axiom 自主开发的数学证明系统 AxiomProver 协调运行。项目采用了不断调整的多模型组合，但没有公开具体的底层模型名单。相比依靠单个模型完成推理，这套系统更强调不同 Agent 之间的任务拆解、证明生成和协作验证。 Axiom 有限单群分类定理形式化工程的矩形树图（Treemap），展示了不同数学模块中的 Lean 声明与代码规模。图源：Axiom Math。 开工后不久，一个棘手问题出现了：Agent 能够证明一条数学命题，却

来源只提供摘要，完整内容请打开原文。