Axiom 用 AI 智能体 24 天完成有限单群分类定理形式化并开源

近一个月以来，AI 正逐步探入数学研究的腹地。10 月 6 日，OpenAI 在代码托管平台 GitHub 上一次性公开了 722 份由内部模型生成的数学手稿，涉及数百个开放问题；10 月 26 日，OpenAI 团队又公布了其模型在调和分析、计算复杂性理论和量子场论上的新发现。 AI 产出证明的速度越来越快，如何确认这些证明可信，就成了数学界必须面对的问题。 其中一种应对办法是形式化验证，即借助证明助手 Lean 等工具，把数学家用自然语言写成的证明逐句“翻译”成计算机能够检查的形式语言。论文中常见的“显然”“同理可得”在 Lean 里行不通，任何省略的推导和隐含的条件都必须写明，每一步推理都要经过 Lean 内核的逐条检查才算通过。 10 月 27 日，美国 AI 数学公司 Axiom 公开了一项体量罕见的成果，宣布其 AI 智能体已在 Lean 中为有限单群分类定理（CFSG）完成了完整的形式化。CFSG 的原始证明约 15,000 页，分散在 500 多篇论文中，出自约 100 位数学家之手，是人类数学史上篇幅最长的证明，人称“巨型定理”。 Axiom 的工程师和数学家调度数十个 AI 智能体，用 24 天写出约 4,310 万行 Lean 代码，目前已在 GitHub 将其开源。 图 | Axiom 绘制的有限单群分类定理证明蓝图，中心为分类定理本身，外圈按依赖层级排列各里程碑和定理。（来源：Axiom） 一份没人能读完的证明 数学家用“群”描述对称性。一个正方体有 24 种旋转方式能让它看上去和原来一模一样，这 24 种旋转连同它们的组合规则就构成一个群。整数可以分解为质数的乘积，有限群也可以层层拆解，最终得到无法再拆分的基本单元，即有限单群。 CFSG 给出了所有有限单群的完整名录：素数阶循环群、交替群、16 个由有限域构造的李型群家族，外加 26 个不属于任何家族的“散在群”。其中最大的魔群（Monster group）约有 8×1053 个元素。数学家常把这份名录比作对称性的元素周期表。 列出名录相对容易，难的是证明名录之外再无遗漏。这项工作从 20 世纪 50 年代起步，约翰·汤普森（John Thompson）因奠基性贡献获得 1970 年菲尔兹奖和 2008 年阿贝尔奖。1983 年，群论学家丹尼尔·戈伦斯坦（Daniel Gorenstein）宣布分类完成，但很快有人发现，其中“拟薄群”一类情形只依靠一份未完成的手稿。 这个缺口直到 2004 年才由迈克尔·阿施巴赫（Michael Aschbacher）和斯蒂芬·史密斯（Stephen Smith）用一部 1,221 页的专著补上，2008 年学界又修补了另一处漏洞。这些论文和专著共同构成了如今所说的“第一代证明”。 证明的分散也成了难题：不同年代的论文使用不同的记号和组织方式，结论之间层层引用，弄清它们如何拼接需要深厚的专门知识。 从 20 世纪 80 年代末开始，参与分类工作的学者着手撰写更系统的“第二代证明”，到 2023 年已出版 10 卷，预计至少需要 12 卷，至今仍未写完。与此同时，代数、数论、组合数学乃至数学物理中的大量结论都以 CFSG 为前提。 图 | 有限单群名录，包括循环群、交替群、16 个李型群家族和 26 个散在群。（来源：Axiom，据 S. D. 史密斯整理及《有限群表示图集》） 一家想“形式化验证一切”的公司 Axiom 成立于 2025 年 3 月，创始人兼 CEO 洪乐潼（Carina Hong）是在广州长大的 00 后。她高中时入选广东数学奥林匹克省队，在麻省理工学院（MIT）用三年修完数学与物理双学位，因本科期间的研究获得美国本科生数学研究最高奖项摩根奖（Morgan Prize），并以罗德学者身份赴牛津大学深造，在进入斯坦福大学读博期间辍学创业。 公司的“创始数学家”、数论学家小野健（Ken Ono）2025 年离开弗吉尼亚大学加入 Axiom，洪乐潼本科期间曾在他主持的暑期科研项目中做研究。公司先后完成 6,400 万美元种子轮和 2 亿美元 A 轮融资，估值已超 16 亿美元。 Axiom 把“形式化验证一切”当作使命，其智能体系统 AxiomProver 能调度多个 AI 智能体协同完成大型形式化任务。今年 8 月，团队完成了素数间隙领域“246 定理”的形式化，这一定理表明存在无穷多对相差不超过 246 的素数。 用小野健的话说：世界即将运行在没人读过的代码之上，证明的形式化是应对这一挑战的试验场。 CFSG 把这个试验场推到了极限。它体量最大、结构最分散，真正能读懂全部论证的人却越来越少。项目核心成员瓦西里·伊林（Vasily Ilin）在社交媒体上写道，真正理解这个证明的人大多已经退休或离世。在

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