产品74°
Axiom 用 AI 智能体将 15,000 页数学证明形式化为 Lean 代码
精选理由
100 多位数学家花几十年的证明，AI 智能体 24 天转成 Lean 可验证代码，数学圈真的被改变了。
Axiom 宣布其 AI 智能体在 24 天内将一份 15,000 页的数学证明转化为 Lean 形式化代码，这是数学史上规模最大的证明之一。该证明由超过 100 位数学家历时数十年完成，内容是有限对称性基本构建模块的分类。智能体在人类指导下完成翻译，使每个逻辑步骤都可被计算机验证，并在此过程中修复了错误。
原文 · kimmonismus
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.
