AI 导读
Axiom 宣布完成对有限单群分类定理的完整 Lean 自动形式化，该证明约 15000 页，由上百位数学家跨越数十年积累，是数学史上最大的证明。作者称其 AI 智能体在人类指导下仅用 24 天完成翻译，使每个逻辑步骤可被计算机检验并修复了错误。
推荐理由
原文转述了形式化耗时和规模等关键事实，读者可以据此评估 AI 智能体在大型数学验证中的当前角色。
正文
Axiom says its AI agents formalized a 15,000-page mathematical proof in just 24 days, largest proofs in mathematics.
Built by over 100 mathematicians across decades, the proof classifies the fundamental building blocks of finite symmetry.
With human guidance, the agents translated it into Lean, making every logical step computer-checkable and repairing errors along the way.
AI tackling an entire interconnected body of mathematics, with results others can verify. A major milestone.
We are witnessing history unfold. Again. Every day now.
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.在 X 查看被引用的帖子
来源：Chubby♨️ · x.com