Axiom releases a 16M-line formalization of the entire Stacks Project

Axiom, the AI math company, released a formalization of the entire Stacks Project, a large reference work for algebraic geometry that Axiom calls critical infrastructure underlying modern math. Axiom says the result is 16 million lines, with optimized code quality and the project's highly interconnected structure preserved, and calls it "a mathematical city".

Axiom framed the release as a counterexample to the view that vibecoding at scale produces slop. The post had about 2,000 likes by the afternoon of November 4.