Axiom 智能体集群 24 天完成有限单群分类定理机器验证

Rohan Paul 在 X 上转述称，Axiom 的 AI 智能体集群完成了有限单群分类定理（CFSG）的机器验证，用时 24 天。CFSG 是数学史上最长的证明，40 多年来数学家在其基础上继续工作，但无人能独自核查全部步骤。 按原文数据，这次验证把跨越 500 多篇论文、约 15,000 页的证明转化为 3800 万行以上机器验证代码，并在已发表记录中发现 34 处严重出入。 被引用的 Leo 帖文补充称，CFSG 的形式化证明可能已成为最大的开源项目之一；配图显示 Axiom CFSG 规模达 43.0M 行，约每 37 天翻倍。原文未说明验证方法细节、代码开放方式或出入的具体内容。