三十年难题，AI用24天逐行验完！1.5万页庞大定理被查出34处漏洞

在数学界，有一个定理大到被人戏称为“庞大定理”。 它的证明由大约100位数学家接力完成，散落在500多篇论文中，总篇幅约1.5万页。 如今，总部位于美国旧金山的人工智能初创公司Axiom宣布，已完成这一定理首个完整的计算机验证证明。 公司表示，一群AI智能体连续工作了24天，写下约4310万行代码，把整个论证逐行翻译成计算机可以检查的语言。 这可能是迄今规模最大的一次数学形式化工程。它让人第一次看到，AI可以承担如此浩大的严谨验证工作。 “对称的元素周期表”到底说了什么 这个“庞大定理”的正式名称是有限单群分类定理。要理解它，得先从“群”说起。 群是抽象代数中最基础的概念之一，凡是有对称的地方，就有群的身影。 从晶体结构到粒子物理，从密码学到魔方，群论的身影几乎无处不在。 以一个立方体为例，共有24种旋转方式能让它看起来和原来一模一样。任意两种旋转组合起来，仍是其中一种，而且每种旋转都可以撤销。 这种封闭且可逆的结构就是一个群，一副洗过的扑克牌则是规模更大的例子。 正如整数可以分解成质数，有限群也可以分解成不可再分的“基本零件”，也就是有限单群。 有限单群分类定理给出了所有有限单群的完整清单，因此被数学家称为“对称性的元素周期表”。 这份清单包括几个性质清楚的无穷族，以及26个“特立独行”的例外，称为散在单群。 其中最大的一个叫“魔群”，大约有8乘以10的53次方个元素，还出人意料地出现在数学物理的某些构造中。 物理学家爱德华·威滕曾提出，与魔群相关的一种构造，或许能描述简化“玩具宇宙”中的引力。纯数学与物理世界，在这里意外相遇。 证明这份清单完整无缺，花了几代人的努力。20世纪50年代，理查德·布劳尔提出了核心策略。 1972年，丹尼尔·戈伦斯坦制定了路线图，1983年人们宣布大功告成。 但这一宣布后来被证明为时过早。一个关于“拟薄群”的漏洞直到2004年才补上，此后还陆续发现了一些小问题。 这段曲折的历史本身就说明，靠人脑审核超长证明是多么困难。即使是最顶尖的专家团队，也难免留下盲区。 形式化验证：让机器当最严格的审稿人 一个由这么多人、跨越这么多年写成的证明，几乎不可能由任何一位数学家完整审核。 形式化验证正是为此而生。整个论证被改写成一种名为Lean的语言，每个定义、每个假设、每一步推理都必须写得足够精确。 在这里，没有任何一步可以用“显然成立”一笔带过，计算机会逐行检查。 近年来，Lean已成为数学形式化的热门工具，越来越多数学家开始用它把经典定理“翻译”成机器可检查的形式。 这种不留情面的严格，恰恰发挥了作用。Axiom的AI智能体在原有证明中发现了不少问题。 大多数问题很小，比如笔误、表格标错，或者漏写了某个前提条件。 这些小问题在人工阅读中极易被忽略。但在形式化系统里，任何一个疏漏都会让验证无法通过。 其中有34处问题严重到需要真正动手修补。 最棘手的一处与“非平衡群定理”有关，修补它甚至需要一段全新的数学。 Axiom为此请来了当年参与原始分类工作的群论专家，包括理查德·莱昂斯和罗纳德·所罗门，帮助绕过这个缺口。 由此得到的论证已整理成一项新的、可以单独引用的群论成果。公司还公开了全部错误清单，供数学界参考。 公开错误清单的做法尤其值得称道。它让数学界可以共同检视这些问题，而不是让它们继续隐藏在浩瀚的文献中。 AI做数学：从“像对的”到“确实对” 这件事最值得关注的地方在于：一个被广泛引用、已有四十年历史的定理，其公开记录中仍存在未解决的裂缝。 而发现和修补这些裂缝的，是一个逐行核查的AI系统。 对于一个依赖代代同行评议来建立信任的学科来说，这无疑是一次深刻的提醒。 这并不是说过去的数学家做错了什么，而是说明人类审核能力存在天然上限。机器的加入，正好弥补了这一短板。 今年以来，各大AI实验室纷纷瞄准重量级、可形式化验证的数学成果。 OpenAI声称证明了某种版本的杨—米尔斯存在性问题。OpenAI和Anthropic还在几小时之内，先后报告推翻了指数时间假设。 无论如何评价这些单独的声明，它们指向同一个问题：AI能否从生成“看起来对”的证明，走向生成机器可以认证“确实对”的证明。 更重要的是，这种认证能达到任何人类团队都无法手工检查的规模。 1.5万页的“庞大定理”被AI逐行验完，或许标志着数学研究正在进入人机协作的新阶段。 未来，数学家或许会把更多精力放在提出问题和构建思想上，而把繁琐的逐行验证交给机器完成。 特别