Axiom 发布 1600 万行 Lean 形式化的 Stacks Project
Axiom 把整个 Stacks Project 转成了 1600 万行 Lean 可验证代码，代数几何的地基现在机器能查了，搞数学形式化的人可以看看。
Axiom 发布了对 Stacks Project 的完整形式化版本，共 1600 万行 Lean 代码。Stacks Project 是现代代数几何的基础文献，结构高度互联。这次形式化在转为机器可校验代码的同时保留了原有结构。该项目反驳了大规模 AI 生成代码必然低质量的看法，为 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. Axiom @axiommathai 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 🌆 Your browser does not support the video tag. 🔗 View on Twitter 🔗 View Quoted Tweet 💬 6 🔄 2 ❤️ 14 👀 2376 📊 6 ⚡
