Axiom 用几十个 AI agent 花 24 天把有限单群分类定理证明转成 Lean 代码，查出中间论文证法漏洞并补上新证法

AI 用 24 天让计算机核对完数学史上最长的证明：定理成立，但其中一篇论文的证法有漏洞，AI 换了一种证法补上 一个证明长达 1.5 万页，散落在 500 多篇论文里，几十年来没有一个人从头到尾读完过，它到底对不对？AI 数学公司 Axiom 10 月 26 日宣布，他们用几十个 AI agent 花了 24 天，把这个证明全部改写成计算机能逐步检查的代码，Axiom 说检查已经全部通过。 这个证明对应的是“有限单群分类定理”，外号“巨大定理”，约 100 位数学家花了几十年才完成。 【这个定理讲什么】 先说“群”。一个立方体，你能找到 24 种转法，转完它看起来跟没动过一样。数学家把这样一组“转完看起来不变的操作”叫做一个群，它是研究对称的工具。 整数可以拆成质数相乘，质数再也拆不动。群也一样，可以拆成一些拆不动的基本单位，叫“单群”。有限单群分类定理给出了一张完整清单：所有基本单位，要么属于几个有固定规律的大家族，要么是 26 个不属于任何家族的特例。最大的特例叫“魔群”，元素个数是 8 后面跟 53 个零。 找到这些单群不算最难，难的是证明清单里没有漏掉任何一个。 【为什么要计算机来查】 证明太长，人查不过来，出过错也不奇怪。1983 年，牵头的数学家宣布证明完成，后来发现其中一块根本没写完，直到 2004 年才用一本 1221 页的书补上。 Axiom 用的检查工具叫 Lean。把证明翻译成 Lean 能读的代码后，它会一步一步核对：每一步是不是真的能从前面推出来。人读论文时会默认“这步显然成立”，Lean 不接受，必须写出来。2012 年有团队用类似工具，花了约 6 年才查完这个定理里一篇 255 页的论文。 【查出了什么】 先说结论：定理本身没错，清单还是那张清单。 问题出在中间一篇论文的证法上。整个证明要用到一个叫“不平衡群定理”的中间结论，Axiom 照着数学家 John Walter 1986 年给出的证明来翻译，AI 发现这个证明里引用的一个说法是错的，并举出了具体的反例。好比一道几何题，答案是对的，但书上的解法中间用了一个不成立的条件，解法得换。 Axiom 请教了当年参与原始证明的数学家 Richard Lyons 和 Ronald Solomon，借用 Solomon 1976 年的一套思路，由 Axiom 的 AI 写出一个新证法，绕开

来源：X · 宝玉 · x.com