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