最长数学证明首次被机器完整核验：24天、数十个AI智能体写出4310万行Lean代码
核心概要
有限单群的分类——人类写过的最长数学证明——现在有了第一个完整的计算机核验版本。这份被称为“巨定理”的证明原本散落在五百多篇文章、约一万五千页里，由约一百位数学家在几十年间写成。Axiom Math 的工程师与数学家指挥数十个 AI 智能体，在 24 天里于 Lean 证明助手中生成约 4310 万行代码，并记录下 34 处值得关注的偏差，其中最要紧的一处涉及 Unbalanced Group Theorem，过程还带出一条新的群论定理。
深度剖析
有限单群的分类，也就是数学里列出基本对称“原子”的那份清单，现在有一份完整的、可由计算机逐步检查的证明。 此前这份被称为“巨定理”的论证分散在五百多篇文章、约一万五千页里，由约一百位数学家在几十年间写成；1983 年的完成宣告并不成立，因为 quasithin 群那一个情形依赖一份未完成的手稿，这个缺口直到 2004 年 Aschbacher 与 Smith 的一千二百二十一页处理才补上。 让这次核验站得住的是翻译过程中浮出的具体反例：形式化共记录 34 处值得记录的偏差，其中最要紧的一处是 Unbalanced Group Theorem，Walter 1986 年的论证假定某个运算会把相关的单群留在指定族内，智能体找到了被该族明确排除的反例，项目组随后借助 Solomon 1976 年的极大 2-分量理论补出一条替代论证，并把它写成一条新的群论定理。
难点不在于写出某一条长论证，而在于让几十个并行工作的智能体写出的定义、假设和结论能彼此对接。 项目组用一张从已发表文献整理的证明地图把整件工作拆成 108 个里程碑和约 380 项更小的任务，智能体在 GitHub 议题上认领里程碑、在 Slack 里汇报完成情况，Lean 这一证明助手则把每一步推理写成计算机可以逐条检查的形式，未补齐的环节无法跳过。 随着共享仓库膨胀，智能体写证明的速度超过了 Lean 重新检查的速度，工程师于是把缓存的分块编译结果分发到各台机器上并行复核，并把昂贵的有限计算外置成可单独检查的证书，使检查速度提高了几个数量级。
启示与展望
这份证明覆盖的是第一代证明，形式化目标因此限定在这一代所用的论证上，仍在推进的第二代多卷本目前预计至少十二卷。它面向的是想追查某个结论依赖哪些前提、假设写的是什么的研究者与群论学家，发布方公开了最终定理与检查方式，并表示会与包括 Richard Lyons 和 Ronald Solomon 在内的顾问委员会继续整理勘误。
Lean 检查的是形式陈述的推导，这条陈述本身是否就是所要的分类命题，仍需要人去看它的陈述与定义；形式化是否复现某条历史论证的每一步是另一个问题，Unbalanced Group Theorem 就改走了另一条路线。勘误清单与其中的修正还会继续整理。