Axiom 发布对整个 Stacks Project 的 1600 万行 Lean 形式化，覆盖代数几何的关键基础，并保留高度互联的结构与优化后的代码质量。作者称这是对“大规模 AI 生成代码即粗制滥造”这一普遍印象的有力反例：由人主导的 AI 智能体群体构建了可复用、机器可验证的数学基础，AI 智能体今后可以用它来做数学。
原文说明 Axiom 用 AI 智能体完成 1600 万行 Lean 形式化并保留结构互联，可作为大规模 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!
Most think vibecoding at scale is slop. Here’s a counterexample. Today we release a 16M-line formalization of the entire Stacks Project, critical infra underlying modern math, with optimized code quality and its highly interconnected structure preserved. A mathematical city 🌆在 X 查看被引用的帖子
来源：Chubby♨️ · x.com