Axiom 用 AI 智能体把 Stacks Project 形式化为 Lean
Axiom 把代数几何的 Stacks Project 整个搬进了 Lean，由 AI 智能体协作完成，每个证明都能机器验证，数学圈的人应该看看。
Axiom 宣布完成了 Stacks Project 的 Lean 形式化，这是代数几何的庞大基础体系。该项目由人类主导的 AI 智能体群体协作完成，所有定义与证明相互连接，可被机器逐条验证。某个章节证明的结果可以在其他章节直接引用。Axiom 形容其结构类似卢浮宫玻璃金字塔：单个部件依靠整体拼合才成立。这为 AI 生成数学内容提供了可机器验证的基础设施。
AI-generated code at scale usually gets written off as sloppy. Axiom's new release is a strong counterexample.
Axiom says it has formalized the Stacks Project in Lean, a huge, deeply interconnected foundation of algebraic geometry, turning it into mathematics a computer can check.
The impressive part isn't just the size, it's the structure. Axiom compares it to the Louvre's glass pyramid: individual pieces that only work because they fit together into something much bigger. Every definition and proof has to connect, so a result proved in one chapter can be used in another.
That's what makes it more than a translation. A human-led swarm of AI agents built a reusable, machine-checkable foundation that AI agents can now use to do mathematics.
Congrats to the Axiom team!
