初创公司 Axiom 称，其多智能体系统 AxiomProver 在约 24 天内，将有限单群分类定理（CFSG，俗称「巨型定理」）完整形式化进 Lean，产出约 4310 万行代码，规模据称超过 Linux 内核等大型开源项目；过程中记录数百处异常，含约 34 处重大逻辑偏差，并对不平衡群定理（UGT）中 Walter 1986 年论证的闭包断言给出反例，再与 Richard Lyons、Ronald Solomon 协作补出新结果 Preservation of simple tops。若主张经独立复核成立，将是顶级纯数学里 AI 从验算走向「发现补丁定理」的标志性案例——仍应以形式化仓库与同行审验为准。同类「AI + Lean」叙事可对照本站ETH 证伪宣称与Meta 超大 Lean 库。
CFSG 为何是「巨型定理」
群描述对称性；有限群可分解为不可再分的有限单群。CFSG 给出「对称性周期表」：素数阶循环群、至少 5 个符号的交错群、16 个李型无限家族，以及 26 个零散群（最大者称魔群）。自 1950 年代起，约百位数学家在 500 余篇论文中拼出约 15000 页证明；1983 年 Gorenstein 宣布完成时仍有缺口，至 2004 年才由 Aschbacher 与 Smith 用约 1221 页补上。证明过长使人类极难通读与零差错——这也是形式化动机。
24 天蜂群：拆地图、写 Lean、顶住依赖瓶颈
据 Axiom，2026 年 10 月 1 日在 Slack 启动；人类将证明拆为约 108 个里程碑、约 380 个小任务形成「证明地图」。10 月 2 日起智能体分工：领头拆解难证、其余检索与写 Lean，缺前置条件则自动外包，结果汇入共享库。产出过快曾拖垮 Lean 依赖检查，工程师临时做分布式缓存。10 月 10 日称形式化「魔群是单群」；全程约 24 天、约 4310 万行 Lean。Ken Ono 等公开表达情绪性反应，属个人见证，不替代技术审计。更多动态见AI资讯。
人机补丁：UGT 断链与新定理
自然语言证明中的「显然」「同理」在 Lean 中站不住。扫描中除笔误与表格错误外，约 34 处重大偏差；关键一环落在 UGT（由局部子群结构推断整体）。以 Walter 1986 文献为基础形式化时，智能体判定关键闭包断言不成立，并给出反例 PSL₂(49)（涉及梅森素数 7 等排除情形）。团队未改用整套「第二代证明」以免推倒既有依赖，而是连线 Lyons、Solomon，基于 Solomon 1976 年思路设计新路线，再由 AxiomProver 形式化 Preservation of simple tops，以导出分类所需的 UGT 形式——定理结论仍成立，证明路径已含 AI 主导补丁。这类似 Voevodsky 转向机器验算的历史动机：复杂证明仅靠人类互审不可靠。
常见问题
Q：CFSG 被形式化是否等于定理刚被「首次证明」？ A：否。分类工作已由人类完成数十年；此次重点是机器可检查的 Lean 形式化，以及过程中发现并修补的论证缺口。
Q：「最大开源项目」如何理解？ A：按 Axiom 所称 Lean 代码行数对比 Linux 等；需以公开仓库与统计口径核实，且行数不等于科学影响力。
Q：AI 是否独立发现了新数学？ A：据方称，新定理路线由人类大师与系统协作构思，再由 AxiomProver 完成严密形式化；宜表述为「人机协作补丁」，并以论文/仓库为准。
相关文章
