Axiom Math has formally verified the Stacks Project, a massive 7,654-page mathematics library, using its proprietary AI agents. The startup translated the entire library into 16 million lines of Lean code to ensure the logical soundness of the proofs. This achievement fills a significant gap in formalized mathematics, specifically covering the complex field of algebraic geometry.
The verification project was led by Axiom CEO Carina Hong, a 25-year-old Stanford dropout who founded the company in March 2025. She raised a $200 million Series A round in the same month, led by Menlo Ventures. Axiom developed its own models to teach agents a ‘human sense of taste’ for formalizing proofs and handling this unprecedented scale.
The verified code serves as a foundational substrate for future AI agents to build software and scientific discoveries upon. Hong challenged other coding companies to undertake formalization at this scale. This breakthrough provides a reliable base for developers to trust automated systems with complex logical structures.
