Axiom Math, a $1.6 billion startup founded in March 2025 by Stanford math PhD dropout Carina Hong, aims to tackle the surge of unreliable AI-generated mathematics by creating a rigorously verified foundation for the field. The company's breakthrough announcement in November 2026 revealed the formal verification of the Stacks Project, one of the largest and most respected compendiums of mathematical knowledge, encompassing topics from algebra to number theory. This rare achievement involved translating the project’s 7,654 pages into 16 million lines of code using the Lean programming language, which is then checked for logical consistency by a proof assistant.

The Stacks Project, initiated by Columbia mathematician Johan de Jong in 2005, is often compared to the Bourbaki books that restructured mathematics in the 20th century, making this verification milestone a significant step in formalizing advanced math. Axiom’s approach involved deploying a fleet of AI agents operating in a loosely structured, parallel manner to maintain the intricate relationships and dependencies between theorems and definitions, something that had initially seemed nearly impossible. Co-founder Ashvin Swaminathan explained that these agents autonomously selected tasks and preserved the delicate hierarchical connections critical to ensuring the consistency and reliability of the work.

Beyond the pure mathematical community, Axiom intends for its verified body of knowledge to serve as a dependable foundation for software development and AI-driven scientific research. With AI increasingly writing code, the company sees formal verification as essential for preventing bugs and security flaws in the future’s complex systems. The startup’s focus on formalizing parts of algebraic geometry addresses a significant gap in existing verified mathematics, providing researchers and AI with a robust base from which to build without starting from zero each time.

CEO Hong highlighted that Axiom’s success with the Stacks Project exemplifies how future AI work will need to rely on a reusable and trustworthy library of verified information to avoid "slop" — careless or error-prone outputs — from compounding over time. She challenged other coding companies to pursue large-scale formal verification projects, arguing that it is crucial for AI agents to have solid, verified infrastructural knowledge to efficiently push the boundaries of math and technology moving forward.