Axiom 用 AI 智能体集群 24 天完成 15000 页数学证明的 Lean 形式化
Big win for verifiable AI.
Axiom 宣布完成有限单群分类的 Lean 自动形式化，这份数学证明约 15000 页、由 100 多位数学家跨代完成，改写后约 4000 万行 Lean 代码，由 AI 智能体集群在数学家引导下用 24 天写出。Axiom 称今年年初让 AxiomProver 写出正确的 1 万行 Lean 证明还需数周反复引导，此次规模约为其 4000 倍，并将跃升归因于同时重建模型、harness 和基础设施三层。
查看原帖人类历史上最大的数学证明现已通过计算机验证。 今天，Axiom 宣布有限单群分类——即“对称性的元素周期表”——的完整 Lean 自动形式化已经完成。 约 15,000 页，由 100 多位数学家跨代共同构建。https://t.co/Y1P26abyPQ
查看原文
The largest math proof in human history is now computer-verified. Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry." About 15,000 pages, built by over 100 mathematicians across generations. https://t.co/Y1P26abyPQ
正文 · AI 翻译
可验证 AI 的重大胜利。
形式化数学证明正开始像软件一样规模化。
@axiommathai 重写了数学史上最长的证明，全部 15,000 页，约 4000 万行 Lean 代码。 成群的 AI 智能体在数学家的引导下用 24 天写完了它。
Axiom 表示，今年年初，让 AxiomProver 写出一个正确的 1 万行 Lean 证明还需要数周的反复引导。而现在，这群智能体在 24 天内形式化了一个规模约为其 4000 倍的问题。
目标是有限单群分类：约 15,000 页、500 多篇论文、约 100 位作者，且没有任何一位读者通读过全部内容。
Axiom 将这一跃升归功于同时重建了三个层面：模型、harness 和基础设施。