THE CRUNCH
Axiom Math, a $1.6 billion startup founded in March 2025, has formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. The company announced on Wednesday that its fleet of AI agents translated the open-source library's roughly 7,654 pages into about 16 million lines of computer-checked code.
Formal verification means rewriting proofs in a programming language called Lean, where a proof assistant checks the code line by line. If a proof passes, mathematicians can trust it is logically sound. Engineers use the same technique to confirm chip designs work, and researchers in France have used it to catch bugs in software that calculates family benefits.
The Stacks Project, started in 2005 by Columbia mathematician Johan de Jong as an open-source reference, spans results from college-level algebra to advanced work across algebra, geometry and number theory. Its theorems and definitions are interconnected, each building on those before it, which made Axiom unsure the project would work at first. The team had to keep every connection intact across the about 16 million lines of code. "Things that are big and things that are delicate in life just don't go together," CEO Carina Hong told TechCrunch.
To pull it off, Axiom gave its agents a loose hierarchy and let them run in parallel, finding their own tasks. The company also trained its own models to be good at math, an approach Hong said most other verification startups have not taken. Technical staff member Ashvin Swaminathan said formalized maths has long had a "huge black hole" covering algebraic geometry, leaving researchers with little to build on in Lean. "Well, now they do," he said.
Axiom's ambitions go beyond mathematics. It argues that each verified result becomes a building block, and that software of the future, written increasingly by AI agents, will need to rest on verified foundations. "Our Lean formalization is now the substrate that agents can build upon," Swaminathan said.