Axiom Math 用 AI 智能体形式化有限单群分类，43.1M 行 Lean
Axiom Math 发布了有限单群分类（CFSG）的完整 Lean 形式化，官方说法是「首个完整的、由计算机检查的证明」。这份被称为「巨大定理」的第一代证明约有 15,000 页、分散在 500 多篇论文里，由约 100 位数学家历时数十年写成，结论是每个有限单群必属于素数阶循环群、交错群、李型群或 26 个散在单群之一。项目从 10 月 1 日开 Slack 频道算起，用 24 天、由数十个 AI 智能体并行推进，产出约 4,310 万行 Lean 代码，每一步逻辑都由 Lean 内核检查。
比「把旧证明搬进机器」更有意思的是过程副产品：形式化暴露出文献里的问题，多数是笔误、表格错误或漏写前提，但有 34 处是需要实质处理的偏差，最大的一处牵涉 Unbalanced Group Theorem——形式化过程中找到了一个闭包断言的反例，论文给出这个障碍与替代论证，改用 Solomon 1976 年的极大 2-分量理论，关键一步是其中 Theorem 2.3（简单顶的保持）。也就是说，这次工程产生了一个群论新结果，团队表示会与相关专家一起公布勘误清单。
需要保留的边界：所谓「检查」是 Lean 内核对其代码的检查，我本人没有独立编译该仓库，也没有逐页读完 blueprint；项目由 Axiom 自建的 agent 蓝图驱动（蓝图、Lean 代码与论文引用都在 GitHub 的 AxiomMath/CFSG）。这件事的意义不在于「AI 证明了 CFSG」，而在于「数十个智能体可以在几周内把一个几万页的人类证明逐句翻译成可机器验证的形式」，而形式化的副产品是找出人类文献里的错。
原文链接：Axiom Math 官方博客
核验记录
日期：单篇文章页 /research/the-enormous-theorem-formalized/ 的可见 meta 为 October 26, 2026，CMS 内嵌记录 article_date 同为 2026-10-26；同页 publishedAt/updatedAt 为 2026-10-27T14:42:53Z（CMS 写入时刻），按 R14 取文章自述日期 10-26，CMS 发布时刻记在此处备查。数字均取自该页正文（135,402 字节直读 200）：「约 15,000 页、500 多篇论文、约 100 位数学家」「24 天」「数十个 AI 智能体」「约 4,310 万行 Lean 代码」「34 处 noteworthy deviations」；「首个完整计算机检查证明」是官方表述，非第三方认证。未做的一环：没有独立 clone 并编译 AxiomMath/CFSG 仓库，也没有通读 blueprint 页面（353,658 字节，只读了正文段落），故正文只写「由 Lean 内核检查」而不写「已被独立验证」。配图取该页 og:image（PNG 1200×1200、855,081 字节），裸请求与带站内 Referer 双 200。
← 上一篇AI 智能体 12 小时摸进 Anthropic 内部系统：薪资、Slack 消息被看到下一篇 →Mirendil 首发 Fern 0.1：从零预训练的 10M 上下文模型，检索撑住、推理掉队