AI仅用24天完成巨型数学定理形式化 揪出40年旧漏洞

一项由顶尖数学家耗费数十年完成的数学证明工程，如今被AI在短短24天内完成了计算机可验证的形式化，这就是有限单群分类定理——数学史上最庞大的证明工程之一。

过去，100多位顶尖数学家参与这项研究，耗时数十年写下1.5万页证明，直到2004年才补上关键缺口，而AI仅用24天就将这项人类数学成果转化为4300多万行可由计算机逐步验证的代码，还揪出了存在近40年的论证漏洞。

要理解这项工作的价值，得从数学中的“对称性”概念说起。数学家将正方形旋转90度后重合的操作及其组合构成的结构称为“群”，群论是研究对称性的通用语言。复杂的有限群可以分解为更基本的部分，如同整数分解为质因数，这些不可拆分的“基本粒子”就是有限单群。

有限单群分类定理要回答一个核心问题：所有有限单群到底有哪些？最终清单包含素数阶循环群、交错群、16个无穷系列的李型单群，以及26个特殊的“散在单群”，其中最大的“魔群”拥有约8×10^53个元素，光是证明它的存在就曾是数学界的重大成就。

10月，某AI数学研究团队宣布，数十个AI Agent在24天内完成了这一定理的形式化，生成约4310万行代码、205万个形式化声明，提供了第一份覆盖整个分类定理的计算机检查证明。原本分散在500多篇论文中的数学推理，被组织成一套可逐步核查的形式系统，过程中Agent不仅发现了历史论文的错误，还构造了一项新的群论结果。

这项工作并非让AI一次性处理全部1.5万页内容，而是从已有基础库和文献中整理出108个里程碑、约380项具体任务，让Agent分工拆解定理、搜索已有结果、生成形式化证明、审查命题并整合代码，人类数学家处理关键障碍，工程师协调系统运行。

项目初期遇到不少挑战：Agent能证明某条命题，却未必是项目真正需要的，比如要求证明桥能过重型卡车，Agent却增加“桥墩足够坚固”的前提，还顺利证明了卡车通行，却忽略了桥墩的前提未被证明，团队不得不删除数万行基于错误假设的代码，重新安排工作。

随着代码库膨胀，形式化验证工具的检查速度跟不上Agent产出，工程师引入共享构建缓存和并行验证机制，让Agent复用已确认的结果。尽管过程中任务拆分的复杂度曾让进度放缓，团队调整策略，将复杂证明拆分为更小的明确任务，要求Agent说明小证明如何组合成最终结论。

更惊人的发现来自对历史文献的核查：Agent发现旧数学论文存在错误。人类数学家常省略熟悉的推理，但形式化要求明确每个前提，团队统计有34处文献偏差需要处理，包括笔误、遗漏条件甚至实质性错误。

其中一个典型案例是关于“拟薄群”的研究，原文引理断言两个量相等，Agent借助群结构找到反例，团队修正引理并扩大论证范围。更大的障碍来自1986年关于“不平衡群定理”的研究，Agent找到反例，虽未推翻定理，但需要另找依据，团队咨询群论专家后，Agent构造并形式化了新的群论结果“简单顶保持定理”，完成了分类所需的证明，虽然后续发现有更短路径，新结果仍被保留。

最终，这项工作的成果被公开，代码不含未完成证明的占位符，仅依赖标准公理，可由形式化工具内核逐步检查，还提供了交互式证明依赖图，让研究者追踪结论的来源。这项工作的基础包括已有形式化项目的成果，人类研究成果、早期基础设施与AI Agent共同构成了这套工程流程。

对数学研究而言，这项工作的关键改变是证明可被持续维护。过去引用有限单群分类定理常牵连数百篇文献，现在研究者可沿着形式化依赖链，检查具体定义、条件和推导。形式化工具让数千万行证明的逻辑接受统一机械化检查，这是过去难以实现的能力。

回望24天的工程，最值得关注的并非AI生成了多少代码，而是它开始处理过去高度依赖人类专家的大规模研究：拆解任务、追踪证明、发现旧文献错误，还参与构造新证明。数十年积累的数学知识，正从散落在论文中的论证，变成可被程序检查、复用和扩展的结构，这是AI参与数学理论建设的重要尝试。