Axiom Math Verifies 7,654-Page Stacks Project, Building 16 Million Lines of Checked Code
Updated
Updated · TechCrunch · Nov 5
Axiom Math Verifies 7,654-Page Stacks Project, Building 16 Million Lines of Checked Code
2 articles · Updated · TechCrunch · Nov 5
Summary
Axiom Math said it has formally verified the Stacks Project, turning the open-source algebraic geometry reference into about 16 million lines of Lean code checked line by line by a proof assistant.
The $1.6 billion startup framed the milestone as a defense against AI-generated math "slop," arguing that agents need reusable, verified building blocks instead of unchecked proofs and code.
Stacks, started in 2005 by Columbia mathematician Johan de Jong, spans roughly 7,654 pages and is one of the largest human-written bodies of mathematics ever formalized.
Axiom said its agents worked in parallel under a loose hierarchy and were trained on in-house math models, helping preserve the project's dense web of interdependent theorems and definitions.
The result fills a major gap in formalized algebraic geometry and supports Axiom's broader bet that verified math can become infrastructure for AI-written software and, eventually, scientific work.