Axiom Math AI Agent完成巨型定理形式化

发生了什么

据凤凰网·科技报道，AI数学公司Axiom Math于10月26日宣布，由人类数学家与数十个AI Agent组成的团队，在24天内完成了有限单群分类定理（巨型定理）的Lean形式化。该项目将原本分散在500多篇论文中的推理转化为约4310万行代码及205万个形式化声明，形成了首份覆盖该定理的计算机检查证明。此外，AI在验证过程中发现了一个存在近40年的论证漏洞，并参与构造了新的群论结果。