AxiomMath Verifies Stacks Project to Keep AI Slop Out of Math

Axiom Math, a startup valued at about $1.6 billion, has formally verified the Stacks Project, one of the largest collections of mathematical work ever produced by humans, in a move it says is designed to prevent unreliable AI-generated mathematics from undermining the field. The project, launched in 2005 by mathematician Johan de Jong at Columbia University, serves as an open-source reference covering areas including algebra, geometry and number theory, ranging from foundational material to advanced research-level results. Axiom’s system used a fleet of AI agents to translate roughly 7,654 pages of human-written mathematical content into about 16 million lines of Lean code, a programming language used for formal proof verification. A proof assistant then checked the code line by line to confirm that each theorem and definition was logically consistent. Because the Stacks Project is highly interconnected, with results building on earlier definitions and theorems, Axiom said the verification required preserving the structure of the material across millions of lines of code. The company’s approach gave its agents a loose hierarchical framework and allowed them to work in parallel, identifying and completing tasks independently. Axiom also developed its own mathematics-focused models to improve the agents’ ability to handle Lean proofs, a step the company says many formal verification startups have not taken. The result fills a major gap in formalized mathematics, particularly in algebraic geometry, where researchers previously had limited machine-checked foundations to rely on when validating new work. Axiom CEO Carina Hong said the broader goal is to create a trusted, reusable foundation that AI agents can use to write software and eventually conduct science. As AI systems generate more code and mathematical claims, the company argues that formal verification can help ensure new work builds on reliable results rather than unverified assumptions. UCLA mathematician Terence Tao has previously argued that the more formalized proofs are available, the more new formalized proofs can be created. For developers, the work points toward a future in which AI-written software can be checked against mathematically sound foundations. Hong said agents will need well-built, reusable knowledge bases to expand capability without being led astray by poor design choices or unreliable outputs. Axiom’s verification of the Stacks Project is therefore both a mathematics milestone and a proof of concept for its larger bet: that trustworthy AI systems require verified infrastructure, starting with the foundations of mathematics itself.