AxiomMath has announced that it has formally verified the Stacks Project, one of the largest mathematical reference works created by humans. The company says the roughly 7,654-page library was translated into about 16 million lines of Lean code, which were checked line-by-line by proof assistants.
What the Stacks Project is and why it matters
The Stacks Project was started by Johan de Jong in 2005 as an open-source reference, and many mathematicians have contributed since. Its content ranges from undergraduate-level algebra through advanced results across algebraic geometry and number theory. Some commentators, such as Peter Woit of Columbia University, consider the project unusually important, likening it to the Bourbaki books that restructured mathematics in the 20th century.
How formal verification works
Formalization involves rewriting mathematical proofs as code in the Lean programming language, then using a proof assistant to verify the code’s logical correctness step by step. Passing that check gives mathematicians confidence the proof is logically sound. Formal verification is also used in industry—for example, to confirm chip designs and to find bugs in social-benefit calculation software.
Technical and organizational challenges
A distinguishing feature of the Stacks Project is the dense network of interdependent theorems and definitions: many results build on earlier ones, so all connections had to be preserved in the Lean sources. That made AxiomMath initially unsure the project could be completed. To succeed, the team deployed a fleet of AI agents working in parallel under a loose hierarchy that preserved structure without micromanaging every agent’s actions.
Ashvin Swaminathan, a member of AxiomMath’s technical staff, said agents identified tasks themselves and worked in parallel. The company also trained its own models specifically for mathematical tasks—an approach AxiomMath’s leadership says is less common among other formal-verification startups. At first, a human Lean expert taught the agents a sense of taste; over time, the agents reportedly developed that capability autonomously.
Leadership and funding
AxiomMath’s CEO is Carina Hong, who is 25 years old and left a Stanford mathematics Ph.D. program before founding the company in March 2025. In March, AxiomMath raised a $200 million Series A round led by Menlo Ventures. The reporting characterizes the company as having around a $1.6 billion valuation.
Why this matters beyond pure mathematics
AxiomMath argues that each verified theorem becomes a reliable building block, so future proofs can build on checked results rather than starting over. As UCLA mathematician and Fields Medalist Terence Tao put it succinctly: the more formalized proofs you have, the more you can produce.
Developers are another intended audience: guaranteeing bug- and vulnerability-free code becomes harder as AI agents write more software. AxiomMath is betting that future software will need verified foundations similar to the way verified mathematics now underpins the Stacks Project.
Future outlook and challenge
Carina Hong and the technical team expect that much future AI work will proceed with agents operating in parallel and picking their own tasks, and that such agents will need well-built, reusable knowledge bases to avoid producing sloppy results. Hong has publicly challenged other coding companies to pursue formalization at comparable scale.
Implications
Formally verifying the entire Stacks Project is a significant milestone for mathematical formalization: a large, checked library can lower the barrier to formalizing new results and can serve as a substrate that AI systems and developers build upon. Over time, this could affect both the methodology of mathematical research and the reliability of AI-generated software.
