← 返回 Sardaana AI
Axiom 称 AI 智能体集群在 24 天内用计算机验证了数学史上最长的证明——有限单群分类
该初创公司发布了约 4310 万行的「巨型定理」Lean 形式化证明，并报告与已发表文献存在 34 处值得注意的偏差。目前尚无外部团队独立重建该证明。
AI 初创公司 Axiom 表示，已完成**有限单群分类定理（CFSG）**首个完整的计算机验证证明。该定理列出了有限对称性的全部「原子」，其原始人工证明由约 100 位数学家在 500 多篇论文中完成，总计约 15,000 页。
如何完成
根据 Axiom 10 月 26 日的报告，工程师和数学家指挥由数十个 AI 智能体组成的集群工作了 24 天（自 2026 年 10 月 1–2 日起），在可逐步检查逻辑的证明助手 Lean 中生成约 4310 万行代码。工作沿用「第一代」证明，基于 Mathlib，分为 108 个里程碑和约 380 项任务。期间智能体还证明了魔群（Monster）是单群。
机器发现了什么
文献中发现的大多数问题较小（错别字、表格错误、遗漏假设），但 Axiom 报告与已发表记录存在 34 处值得注意的偏差。最大的一处涉及非平衡群定理：智能体在 John Walter 1986 年论证的一个步骤中找到反例；在咨询群论学家 Richard Lyons 和 Ronald Solomon 后，团队构建了替代路径，其中包括其证明器得出的一个新结果。Axiom 表示将公布勘误清单。
注意事项
Lean 负责检查推导，但仍需人工确认形式化陈述和定义确实表达了预期的定理。据截至 10 月 27 日的媒体报道，尚无外部团队独立重建完整证明；Axiom 已公开代码库和构建产物以便复现。以上说法来自公司自己的报告。