AI 完成有限单群分类定理形式化验证 数学家动情落泪

初创团队 Axiom 研发的多智能体系统 AxiomProver 仅用 24 天就完成了百余名顶尖数学家耗费大半个世纪写下、长达 15000 页的有限单群分类定理（即「巨型定理」）的形式化验证，构建出超 4300 万行的 Lean 代码库，成为当前规模最大的开源软件项目。该定理是为所有有限单群开出的「元素周期表」，在数学乃至物理领域都有重要价值，此前因证明过于庞杂，人类难以完整通读且容易出错。AI 在形式化过程中排查出数百处异常，其中 34 处为重大逻辑偏差，核心漏洞出现在关键的不平衡群定理相关论证中，AI 还给出了对应反例。后续团队联合资深群论学者构思新的证明路线，由 AI 主导证明了全新的群论结果作为补丁，成功修补漏洞完成验证，这也是 AI 首次在顶级纯数学研究中成为发现新定理、修补核心漏洞的核心合作者。