一份可以被机器逐行验证的证明
10 月 26 日，AI 数学公司 Axiom Math 公布了一项工程：由人类数学家与工程师指挥的数十个 AI agent，在 24 天内完成了有限单群分类定理（Classification of Finite Simple Groups，CFSG）的 Lean 形式化，产出约 4310 万行 Lean 代码、205 万个形式化声明，并给出一份覆盖整条分类定理、可由计算机逐步检查的证明。这条定理被数学界称为「巨型定理」，是人类数学史上篇幅最庞大的成果之一。
形式化（formalization）与通常的「AI 写出解答」不是一回事。Lean 是一种证明辅助语言，它的内核会对每一步推导做机械化检查——只有能被内核确认的逻辑步骤才被接受。换句话说，这份 4310 万行代码不是「看起来对」的草稿，而是每一行都经过机器核验、最终不含 sorry（Lean 里临时跳过未完成证明的占位符）的完整证明工程。对依赖数百篇文献、跨越数十年记号的数学结论来说，能被统一、机械地检查，本身就是一次质变。
24 天，从 1.5 万页到 4300 万行
这条定理的证明原本分散在 500 多篇论文里，正文累计约 1.5 万页。Axiom 从 10 月 1 日开始，先把已发表证明切成 108 个里程碑、约 380 个小任务，再以 GitHub issues 的方式分发给 agent 认领：一个 agent 认领任务、把前置结果交付给另一个 agent，形成并行推进的工作流。早期部分里程碑藏着巨大的隐含假设，团队为此丢弃了数万行建立在错误前提上的成品；10 月 13 日前后，一度只有 1 个里程碑收尾，构建时间成为新瓶颈，工程师把重计算搬到独立校验的证书上、跨机器缓存结果才把节奏拉回来。
体量上，这次工作是迄今规模最大的计算机检查证明。作为参照，Georges Gonthier 团队 2012 年形式化 255 页的 Feit–Thompson 定理花了六年；Axiom 在 24 天里覆盖了体量大得多的对象，不过公司明确把功劳分给更早的 Lean 库与约 120 万行既有代码。最终结论只依赖标准公理，并可由 Lean 内核逐步检查；Axiom 同时公开了交互式证明依赖图，让研究者追踪一个结论究竟依赖哪些前置定理。
不止翻译：agent 揪出了 40 年前的论证漏洞
更值得注意的，是 agent 在搬运旧文献时发现了问题。Axiom 说，大部分偏差只是笔误、表格错误或漏写假设，但有 34 处对原文足够严重的偏离需要真正解决；其中分量最重的一处指向 John Walter 1986 年证明中的一个步骤——具体反例出现在某个闭包论断里，定理本身未被推翻，但在群论专家 Richard Lyons 与 Ronald Solomon 的建议下，证明团队改写了论证，并额外产出了一条新的群论结果（后被写入一篇 35 页论文的定理 2.3）。后来 Axiom 自己的数学家又找到更短的路径，可以绕开这条新定理得到目标结论，但新定理与完整证明仍被保留下来，成为这次工程意外产生的数学成果。
「AI 检查出人类证明里的错误」并不新鲜，但这次的尺度不同：不是单篇论文里的个别失误，而是横跨数十年、数百篇文献的庞大体系，在逐行机器检查下暴露出可被具体反例定位的缺口。对数学研究而言，这意味着证明从「引用一篇可能出错的论文」变成「沿着可检查依赖链追溯定义、条件与推导」。
为什么这件事超出「AI 做数学题」
过去一年，AI 在数学上的进展多以「解题」面貌出现：在竞赛题、形式化基准或单篇证明上拿分。Axiom 这次展示的，是 AI agent 参与整套数学理论的「建设」——拆解任务、追踪证明、发现旧文献的错误，并在旧路线走不通时参与构造新证明，而不是只回答一道具体题目。数十年积累的数学知识，正从散落在论文里的论证，变成可被程序检查、复用与持续维护的结构。
这背后是工程方法论的变化：把一份巨型证明当成可并行、可审计、可回滚的软件项目来管理。GitHub issues 认领、Slack 汇报、agent 互相评审，这些原本属于软件工程的协作模式，被直接搬进了数学形式化的现场。
需要冷静的地方：自评、可审计，但尚无外部审计
也要把话说清楚。目前所有数字都来自 Axiom 自己的研究帖，文中没有提到外部独立审计；仓库的审查状态被标为「团队自评」。Lean 检查的是推导是否自洽，并不检查形式化陈述是否准确对应原命题——最终仍要由外部数学家判断这些定义与选择是否忠实地表达了分类定理。一旦 errata 清单公开，群论专家可以自行核对 Axiom 给出的 34 处偏离是否成立，对这种方法的首份外部裁判也会来自他们。
另一个现实约束是算力与成本：这类工程依赖大量 agent 并行运行与高吞吐构建，门槛并不低。它能复制多少、能否成为数学研究的常态工具，取决于形式化基础设施、模型可靠性与人力协作模式的共同成熟，而非单次演示。无论如何，这次 24 天把「巨型定理」变成机器可检查代码，已经把 AI 参与数学研究的边界往前推了一段。