Axiom Math says it has formally verified the Stacks Project, a large open-source reference covering algebra, geometry, and number theory. The project began in 2005 under Columbia mathematician Johan de Jong and has grown through contributions from mathematicians. Axiom’s agents translated its roughly 7,654 pages into about 16 million lines of computer-checked Lean code.
Formal verification rewrites mathematical proofs as code that a proof assistant checks line by line. The challenge for Stacks extended beyond validating individual theorems: its definitions and results depend on one another, so Axiom had to preserve those connections across the full codebase. The company used a loose hierarchy while allowing agents to identify tasks and work in parallel.
Axiom also trained its own models for mathematics. Initially, an in-house Lean specialist guided the agents on how to approach the work. The company says the completed formalization fills a major gap in algebraic geometry, giving researchers a checked body of prior work on which to build future proofs.
The startup sees the effort as relevant beyond mathematics. Formal verification is already used to check chip designs and software, and Axiom argues that reusable verified foundations could become more important as AI agents write more code. CEO Carina Hong founded the company in March 2025 after leaving a Stanford mathematics PhD program. Axiom raised a $200 million Series A in March and was valued at $1.6 billion.