The artificial intelligence startup Axiom Math has announced the success of its system of autonomous agents in formally and programmatically verifying (Formal Verification) the entire content of the Stacks Project, which is considered one of the largest open mathematical references authored by mathematicians throughout history.
Converting mathematical knowledge into auditable code
The Stacks Project, initiated by Columbia University mathematics professor Johan de Jong in 2005, contains approximately 7,654 pages covering principles of algebra and algebraic geometry, extending to advanced theories in number theory. Axiom Math's swarms of agents were able to translate these complex and interconnected texts into approximately 16 million lines of code in Lean, a specialized programming language that allows verification software to review every mathematical proof line-by-line to ensure its rigorous logical integrity.
The company, which has a market valuation of $1.6 billion after raising $200 million in a Series A funding round led by Menlo Ventures, aims to build a reliable and programmatically proven knowledge base. This base will be used by future AI systems in software development and scientific research to avoid producing misleading or inaccurate conclusions known as AI slop.
The mechanism of software agents and structural coherence challenges
Carina Hong, the company's 25-year-old founder and CEO who left her PhD program in mathematics at Stanford University to establish Axiom in March 2025, explained that the greatest challenge was maintaining the coherence of thousands of theories and avoiding any conceptual contradictions. For his part, Ashvin Swaminathan, a member of the company's technical team, noted that the AI agents did not work under direct guidance for every step; rather, they were provided with a flexible hierarchical structure that allowed them to distribute tasks in parallel and utilize specialized models trained on sound mathematical reasoning instead of relying on general code-generation models.
What this achievement means for the technology sector
This development represents a practical step toward bridging a major gap in computational mathematics, especially in fields such as algebraic geometry. The benefit of formal verification is not limited to academic circles; documenting proofs via computer code provides a reusable foundational environment. The company is betting that developers and creators of sensitive software—such as chip design and critical system calculations—will need these verified bases to prevent security vulnerabilities and hidden errors resulting from the increasing reliance on agents to write software.