Axiom Math 用数十个 Agent 在 24 天内完成有限单群分类定理的 Lean 形式化，并发现 40 年前的证明漏洞
这是 AI 首次把人类最庞大的数学证明整体搬进可机器验证的形式系统，并在过程中反过来挑出人写的证明错误。
100 多位数学家耗时数十年、写下约 1.5 万页证明的有限单群分类定理，被 Axiom Math 组织的数十个 AI Agent 在 24 天内转成约 4310 万行 Lean 代码、205 万个形式化声明，这是首份覆盖整个定理的计算机可检查证明。过程中 Agent 还查出历史论文里约 34 处偏差，其中包括一处存在近 40 年的论证漏洞。
正文摘录
.jpg) 编辑｜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 万个形式化声明 ，给出了第一份覆盖整个分类定理的计算机检查证明。