Axiom Math announced it had formally verified the Stacks Project, a large body of human-written mathematics, translating its roughly 7,654 pages into about 16 million lines of Lean code checked by a proof assistant. The company says its fleet of AI agents did the work.
The Stacks Project was started in 2005 by Johan de Jong, a Columbia mathematician, as an open-source reference. It covers results from college-level algebra through advanced ideas in algebra, geometry and number theory.
Axiom CEO Carina Hong told TechCrunch the team was unsure the project would work at first, because its theorems depend on one another and every connection had to stay intact. Hong said, "We were not sure if vibe coding would be able to preserve the beauty of Stacks."
Ashvin Swaminathan, a member of Axiom's technical staff, said the team imposed a loose hierarchy and let agents run in parallel, choosing their own tasks. He said Axiom trained its own models for math, an approach he said most other verification startups have not taken.
Swaminathan said the work fills a gap in formalized mathematics. "When you look at what has been formalized in mathematics, there's this huge black hole. And that black hole covers algebraic geometry," he said.
Axiom argues that verified results can serve as a foundation for future work and for software development, where AI agents increasingly write code. Hong said, "I openly challenge all the coding companies to work on formalization at this scale."