Axiom 用 AI 智能体集群重写有限简单群分类的 15,000 页形式化证明

AI 导读

Axiom 称，AI 智能体集群在数学家引导下用 24 天完成了有限简单群分类约 15,000 页、约 4,000 万行 Lean 的形式化证明。此前写出正确的 10,000 行 Lean 证明还需数周引导，此次规模约扩大 4,000 倍。Axiom 将这一变化归因于同时重建模型、harness 与基础设施三层。

正文 · 原文

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.