Key facts
- AxiomMath said its AI agents translated the Stacks Project's roughly 7,654 pages into about 16 million lines of Lean code.
- The Stacks Project was started in 2005 by Columbia mathematician Johan de Jong as an open-source reference.
- AxiomMath CEO Carina Hong said the team was unsure whether AI coding could preserve the library's structure.
- Technical staff member Ashvin Swaminathan said formalized algebraic geometry had been a gap for Lean users.
- AxiomMath raised a $200 million Series A led by Menlo Ventures in March.
AxiomMath said on November 4 that it had formally verified the Stacks Project, an open-source mathematics reference started in 2005 by Columbia mathematician Johan de Jong. The company said its fleet of AI agents translated the library's roughly 7,654 pages into about 16 million lines of Lean code, a programming language in which a proof assistant checks each line.
Formal verification is the same idea engineers use to confirm chip designs work. For the Stacks Project, checking each theorem was only part of the job: the theorems and definitions build on one another, and AxiomMath said it had to keep every connection intact across the code.
"Things that are big and things that are delicate in life just don't go together," CEO Carina Hong told TechCrunch. "[Stacks] is a collection of mathematical results that is the foundation of mathematics." Hong, 25, dropped out of a Stanford math Ph.D. program and founded the company in March 2025; in March it raised a $200 million Series A led by Menlo Ventures.
Technical staff member Ashvin Swaminathan said formalized algebraic geometry had been a gap for Lean users. "When you look at what has been formalized in mathematics, there's this huge black hole. And that black hole covers algebraic geometry," he said, adding that researchers now have a base to build on.
AxiomMath argues each verified result becomes a building block for future proofs. Hong said she expects AI agents to need a reusable body of knowledge to avoid producing low-quality output, and challenged coding companies to work on formalization at this scale.