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
正文
Big win for verifiable AI.
Formal Math proof is starting to scale like software.
@axiommathai rewrote the longest proof in mathematics, all 15,000 pages, about 40 million lines of Lean. Swarms of AI agents wrote it in 24 days while mathematicians steered them.
Axiom says that at the start of this year, getting AxiomProver to write a correct 10,000-line Lean proof took weeks of coaxing. And now this swarm of agents formalized a problem roughly 4,000 times that size in 24 days.
The target was the Classification of Finite Simple Groups: about 15,000 pages, 500+ papers, around 100 authors, and no single reader who has gone through all of it.
Axiom credits the jump to rebuilding three layers at once: the models, the harness and the infrastructure.