7,654 pages, 16 million checked lines: axiom math wants AI to keep slop out of mathematics | techcrunch
Verifying a major math reference
AxiomMath announced Wednesday that it had formally verified the Stacks Project, an open-source reference started by Columbia mathematician Johan de Jong in 2005. Contributors have expanded it across algebra, geometry and number theory, from college-level material to advanced results.
Axiom’s AI agents converted the project’s roughly 7,654 pages into about 16 million lines of Lean code. A proof assistant checks the code line by line, allowing mathematicians to assess whether a proof is logically sound.
Keeping the connections intact
The project’s theorems and definitions depend on one another, so verifying individual results was not enough. Axiom had to preserve those relationships throughout the code, a challenge the company initially doubted it could handle.
CEO Carina Hong said the team wanted the mathematical foundations to remain consistent. The 25-year-old left a Stanford math Ph.D. program and founded Axiom in March 2025; the company raised a $200 million Series A in March, led by Menlo Ventures.
Agents worked in parallel
Axiom gave its agents a loose structure and let them identify tasks they could tackle simultaneously, said Ashvin Swaminathan, a member of the company’s technical staff. Hong said the company also trained its own models for mathematical work.
The team initially relied on an in-house Lean expert to teach the agents what Hong described as a human sense of taste. She said the agents have gradually developed that ability themselves.
A foundation for future proofs
Swaminathan said algebraic geometry has been a major gap in formalized mathematics. Researchers seeking to check new work in the field with Lean previously had little existing material to build on; he said the Stacks verification changes that.
Axiom says verified results can serve as building blocks for later proofs rather than forcing researchers to start from scratch. UCLA mathematician and Fields Medal winner Terence Tao has likewise argued that more formalized proofs make further formalization possible.
Key points
- AxiomMath says it verified the Stacks Project using Lean and AI agents.
- The project spans roughly 7,654 pages and about 16 million lines of code.
- The verification preserves links among interconnected theorems and definitions.
- Axiom says the work gives algebraic geometry researchers more verified material to build on.