16 Million Lines Formalize the Stacks Project; the Video Shows a Mathematical City

Axiom has released a 16-million-line formalized version of the Stacks Project. Jeff Dean reposted the news. Axiom's claim is blunt: most people think large-scale vibecoding is slapdash, but here is a counterexample.

The Stacks Project is an open reference project in algebraic geometry and algebraic stacks. It is large in scale, with dense cross-references among definitions, theorems, and proofs. Formalizing it means rewriting mathematics written in natural language into machine-checkable code. General readers can understand it as applying machine verification to mathematical proofs, forcing many implicit steps into the open. For readers with a development background, the difficulty is not the line count, but whether the dependency relationships are complete, whether the proofs can be checked, and whether later modifications will trigger cascading collapse.

Axiom says this version preserves optimized code quality and a highly interconnected structure. In the video, this structure is compared to a mathematical city; the relationships between roads and buildings are more informative than raw line count alone.

Sixteen million lines can easily create a stir. What is more worth examining is whether, after large-scale code generation, the structure remains maintainable, whether the proofs really pass checking, and whether the cost of manual review has been shifted elsewhere. If the formalization process relies heavily on model generation, the evaluation metrics should not be just line count; they should also look at the checkable proportion, dependency completeness, refactoring cost, and review cost. That is where the value of Axiom's counterexample lies.

Original link: Jeff Dean reposts Axiom