AI 导读
AI 与数学的重大发布！ 许多人认为大规模 AI 生成的代码意味着低质量。 Axiom 在 Lean 中完成的新 Stacks Project 形式化工作说明并非如此。 Stacks Project 是现代代数几何庞大且深度互联的基础。 他们将其转化为机器可校验的代码，并保持了结构完整。AI 智能体现在有了一个可复用的基础，可以在其上构建新的数学。
正文
Huge release for AI and math!
Many people assume AI-generated code at scale means low quality.
Axiom's new Stacks Project formalization in Lean says otherwise.
The Stacks Project is a massive, deeply interconnected foundation for modern algebraic geometry.
They turned it into machine-checkable code and kept that structure intact. AI agents now have a reusable foundation to build new math on.
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 查看被引用的帖子
来源：elvis · x.com