Axiom 用 AI 智能体集群完成 1.5 万页数学定理的 Lean 形式化证明
Axiom 把 1.5 万页的有限单群分类定理变成了 4,000 万行 Lean 代码，智能体集群 24 天干完，年初这活要几周才能写 1 万行。
Axiom 将数学界最长的证明——有限单群分类定理，约 15,000 页、500 多篇论文——全部改写为约 4,000 万行 Lean 形式化代码。智能体集群用 24 天完成，数学家负责引导方向。年初时 AxiomProver 写一个正确的 1 万行 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.
