Axiom releases a 16-million-line formalization of the Stacks Project
The company pitches it as proof that AI-written code at scale doesn't have to be slop.

Axiom (@axiommathai) released a 16-million-line formalization of the entire Stacks Project, which it calls critical infrastructure underlying modern math.
The company says the code keeps the project's highly interconnected structure while optimizing code quality, and offered it as a counterexample to the idea that vibecoding at scale is slop. It called the result "a mathematical city."
The post drew about 2,200 likes.





