Axiom称，AI 智能体已在 Lean 中形式化有限单群分类定理

AI 数学公司 Axiom 在 X 上宣布，已在 Lean 中完成有限单群分类定理的完整自动形式化，并称这一成果为“对称性的元素周期表”。Axiom称，原始证明约有 15,000 页，由几代 100 多位数学家共同完成，并称这是历史上规模最大的经计算机验证的数学证明。

根据 Axiom 的开源代码库，多个 AI 智能体组成的集群在 24 天内生成了约 4,310 万行 Lean 代码，涵盖 715 篇论文和书籍，并标记出与已发表记录存在的 34 处差异。AI 新闻账号 TestingCatalog 的一则帖子补充称，智能体像软件团队一样分工协作，编写代码的速度甚至超过了 Lean 的检查速度。

这些数据均来自 Axiom 自身的说法；此次公告未包含对该形式化工作的独立审查。截至 10 月 28 日，这则帖子在 X 上获得了约 6,200 个赞。