Axiom Math formally verifies the Stacks Project to give AI a reliable math base

Axiom Math announced on Wednesday that it has completed a formal verification of the Stacks Project, one of the most extensive collections of modern mathematics ever assembled by human authors. By converting the 7,654-page library into roughly 16 million lines of Lean code that a proof-assistant can check line by line, the company claims to have created the first large-scale, machine-readable foundation for artificial-intelligence agents that need mathematically sound reasoning.

The Stacks Project began in 2005 as an open-source effort led by Columbia mathematician Johan de Jong. Over the years, contributors have added results spanning elementary algebra to the most advanced topics in algebraic geometry and number theory. Axiom’s AI agents were tasked with translating each theorem, definition, and proof into Lean, a programming language designed for formal verification. The process required preserving the intricate web of dependencies among theorems, a challenge the team likened to keeping a massive family tree intact while converting every branch into code.

Carina Hong, the 25-year-old CEO, left a Stanford PhD program in mathematics to launch Axiom Math in March 2025. The company raised a $200 million Series A round led by Menlo Ventures earlier this year, bringing its valuation to $1.6 billion. Hong explained that the goal is not to slow AI progress but to provide a “verified foundation” on which future agents can safely build software and eventually conduct scientific research. “You want theorems to be consistent and not paradoxical,” she told TechCrunch, emphasizing the need for internal coherence in any reusable knowledge base.

Axiom’s technical team, including staff member Ashvin Swaminathan, adopted a loosely hierarchical approach for the AI agents. Rather than dictating every step, the company allowed agents to identify tasks they could execute in parallel, creating a self-organizing workflow that maintained the necessary logical connections. The firm also trained its own language models specifically for mathematical reasoning, a strategy Hong says distinguishes Axiom from other verification startups that rely on off-the-shelf models. Over time, the agents developed an internal “taste” for proof style, reducing the need for constant human supervision.

The verification of Stacks fills a notable gap in formalized mathematics, particularly in algebraic geometry, where few Lean libraries existed before. Researchers now have a substantial base of checked results to reference, potentially accelerating new discoveries. As Fields Medalist Terence Tao has observed, each formalized proof expands the pool of proofs that can be built upon, creating a virtuous cycle of rigor and productivity.

Beyond academia, Axiom sees its work as a safeguard for software development. As AI agents write increasing portions of production code, the risk of hidden bugs and security flaws grows. A verified mathematical substrate could enable agents to reason about program correctness with the same confidence they apply to formal proofs. Hong challenged other coding companies to attempt formalization at comparable scale, arguing that early investment in reusable, error-free libraries will determine the quality of AI-generated software in the years ahead.

The company’s next steps involve extending the verified library to additional mathematical domains and integrating the Lean codebase into tools that AI developers can query directly. If successful, Axiom’s approach could become a cornerstone of a new generation of trustworthy AI systems, turning today’s “slop” into rigorously checked knowledge.