1.5万页的有限单群分类定理，AI代理24天翻成了4300万行Lean

数学史上最长的证明，现在被计算机逐行检查了一遍。

有限单群分类定理，大约 15000 页，前后有百来位数学家花了几十年才拼完，散落在几百篇论文里。没有任何一个人能完整读完并确认每一步都对。

数学 AI 公司 Axiom 用了 24 天，指挥成群的 AI 代理，把整个证明转成了 Lean。Lean 是一种形式化证明语言，每一步逻辑推导都由计算机验证，写错一个符号都过不了。

最后产出大约 4310 万行代码。协作方式也挺像一个软件项目：代理各自认领任务，缺的部分丢给其他代理，所有成果汇进同一个代码仓库。

更重要的是它真的找出了问题。大部分是笔误和表格错误，但 Axiom 说有 34 处偏差必须修正。其中 1986 年一篇论文里的某一步存在反例，原来的论证不成立。代理们回头借用 1976 年的思路另走了一条路，顺带证明了一个新的群论结果。

参与原始证明的群论学家在最难的几个部分给了指导，所以这不是纯 AI 单干。

前几天 OpenAI 也放出了一批内部模型生成的数学成果。两件事放在一起看，AI 在数学上的角色正在从“猜答案”变成“验算整个学科的地基”。后者也许不那么吸引眼球，但对数学界的意义可能更大。