ARTICLE · 人工智能
重磅！AI 补全人类史上最大数学证明，数学家当场泪崩
一语总结Axiom 团队利用多智能体系统 AxiomProver，在 24 天内完成有限单群分类定理的全面形式化，构建了超 4310 万行的 Lean 代码库，并成功修复了原始证明中的关键逻辑漏洞，标志着 AI 在纯数学研究中实现了从验证到发现的飞跃。
本文报道了 Axiom 团队在有限单群分类定理（CFSG）形式化工作中的重大突破。通过部署多智能体系统 AxiomProver，团队在 24 天内完成了对 15000 页数学证明的全面形式化，构建了人类历史上最大的 Lean 代码库。在这一过程中，AI 不仅成功识别并修复了原始证明中的关键逻辑错误，还独立证明了新的数学定理来补全缺口，展现了 AI 在纯数学研究中的强大能力。
- AI 完成有限单群分类定理的全面形式化
Axiom 团队使用多智能体系统 AxiomProver，在 24 天内将长达 15000 页的 CFSG 证明转换为可执行的 Lean 代码，构建了超 4310 万行的代码库，这是人类历史上最大的开源软件项目。
- AI 识别并修复原始证明中的逻辑漏洞
在形式化过程中，AI 发现了原始证明中关于不平衡群定理（UGT）的致命逻辑错误，并基于人类数学家的建议，独立证明了新的定理（Preservation of simple tops）来修复这一漏洞，确保了分类定理的完整性。
- 人机协作实现了从验证到发现的飞跃
这一工作标志着 AI 在纯数学研究中的角色从简单的验证工具转变为主动的发现者和问题解决者。AI 能够理解高层次的数学概念，并独立生成新的证明来应对未预料到的挑战。
重磅！AI 补全人类史上最大数学证明，数学家当场泪崩
本文报道了 Axiom 团队在有限单群分类定理（CFSG）形式化工作中的重大突破。通过部署多智能体系统 AxiomProver，团队在 24 天内完成了对 15000 页数学证明的全面形式化，构建了人类历史上最大的 Lean 代码库。在这一过程中，AI 不仅成功识别并修复了原始证明中的关键逻辑错误，还独立证明了新的数学定理来补全缺口，展现了 AI 在纯数学研究中的强大能力。
文章金句
"在 24 个日日夜夜里，这群不知疲倦的 AI 智能体，产出了惊人的 4310 万行 Lean 代码，构建了人类目前最大的 Lean 代码库。
"AI 不仅指出了错误，还给出了一个明确的反例：PSL₂(49)。在这个反例中，一个操作会产生一个被明确排除在目标家族之外的群（因为 7 是梅森素数）。
"AxiomProver（AI 系统）亲自上阵，根据新思路，严丝合缝地证明了一个全新的群论结果——Preservation of simple tops。