Original post · AI translation
完整的官方报告在这里。
可验证人工智能的一大胜利。
形式化数学证明正开始像软件一样实现规模化。
@axiommathai 将数学史上最长的证明全部 15,000 页重写为约 4,000 万行 Lean 代码。
在数学家的指导下，成群的人工智能智能体用 24 天完成了编写。
Axiom 表示，今年年初，要让 AxiomProver 写出一份正确的 10,000 行 Lean 证明，还需要花数周时间反复引导。而现在，这群智能体在 24 天内将一道规模约为其 4,000 倍的问题形式化了。
目标是有限单群分类：约 15,000 页、500 多篇论文、约 100 位作者，而且没有任何一位读者通读过全部内容。
Axiom 将这一飞跃归功于同时重建了 3 个层面：模型、运行框架和基础设施。
Original
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.
人类历史上规模最大的数学证明如今已通过计算机验证。
今天，Axiom 宣布已完成有限单群分类的 Lean 自动形式化；这一分类被称为“对称性的元素周期表”。
约 15,000 页，由跨越数代的 100 多位数学家共同完成。https://t.co/Y1P26abyPQ
Original
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