AxiomMath verifies Stacks Project to curb AI errors
The startup says its AI agents turned the vast Stacks Project into 16 million lines of checked Lean code to build a more reliable base for AI work.
AxiomMath says it has taken a major step toward making AI-generated work more reliable by formally verifying the Stacks Project, one of the largest mathematical libraries ever created. On Wednesday, the startup said its AI agents translated the project into computer-checked code, aiming to create a foundation future AI systems can build on. As IT-PUB News notes, the announcement lands at a time when concern is growing over AI tools that sound confident while still getting things wrong. In mathematics, that problem is especially hard to ignore.
A formal check for one of mathematics’ biggest libraries
On Wednesday, AxiomMath announced that it had formally verified the Stacks Project. The project began in 2005 as an open-source reference started by Columbia mathematician Johan de Jong, and it has since grown through contributions from mathematicians working across algebra, geometry and number theory.
The scale helps explain why the announcement stands out. Axiom said its AI agents translated the library’s roughly 7,654 pages into about 16 million lines of computer-checked code.
Formal verification means rewriting a proof in a programming language called Lean, then having a proof assistant check it line by line. If the proof passes, mathematicians can treat it as logically sound. The same method is also used in other fields, including chip design and some software bug detection.
For AxiomMath, the goal was not simply to digitize a large body of work. It was to preserve the structure of a mathematical system in which theorems and definitions depend on one another, more like branches in a family tree than isolated results.
Why the Stacks Project mattered to AxiomMath
Axiom CEO Carina Hong said the company was not sure at first whether the project would work, because the Stacks Project is both large and delicate. She described it as a foundation of mathematics that needs to stay consistent, with definitions and theorems that do not conflict.
Given the size of the task, that concern is easy to understand. Axiom had to keep every connection intact while working across millions of lines of Lean code.
Hong, 25, founded Axiom in March 2025 after dropping out of a Stanford math Ph.D. program. In March, the startup raised a $200 million Series A led by Menlo Ventures. Together, the funding and the announcement suggest the company is positioning itself as more than a math tool. It wants to build infrastructure for AI systems that need trustworthy building blocks.
Hong also said the team was unsure whether “vibe coding” would be able to preserve the quality of the Stacks Project. That points to a broader issue in AI development: systems can produce output quickly, but speed does not guarantee correctness.
How Axiom’s agents handled the verification
To complete the verification, Axiom gave its AI agents a loose structure and let them work in parallel. According to Ashvin Swaminathan, a member of the technical staff, the team did not control every step of the process. Instead, the agents identified tasks for themselves and split the work among themselves.
The company also trained its own models to be good at math, which Hong said is not common among verification startups. At the beginning, Axiom relied on one of its in-house Lean experts to teach the agents a human sense of taste. Hong said the agents gradually learned that judgment on their own.
Axiom argues that this matters because formalized mathematics still has major gaps. Swaminathan said there is a large “black hole” in what has been formalized so far, and that algebraic geometry is part of it. Until now, researchers who wanted to verify new work in that area with Lean had little existing material to build on. Axiom says the Stacks formalization changes that.
A building block for future software
Axiom’s pitch goes beyond mathematics. The company believes each verified result can become a reusable block for future proofs, reducing the need to start from scratch every time. UCLA mathematician and Fields Medal winner Terence Tao has expressed the same idea more simply: the more formalized proofs exist, the more formalized proofs can be made.
That logic sits at the center of Axiom’s broader strategy. The startup argues that the same verified foundation could eventually support software development, especially as AI agents take on more coding work. Developers already struggle to guarantee that code is free of bugs and security holes, and that challenge grows as AI writes more of the world’s software.
Swaminathan said the company sees mathematics as the place to start because the skill can transfer. In his view, agents should be able to read the code, understand it and build new infrastructure on top of it. Hong made a similar argument, saying AI systems need a reusable library to avoid producing low-quality output and to keep moving forward.
AxiomMath bets AI needs firmer ground
AxiomMath’s message is less about replacing mathematicians than about creating a safer base for machine work. The company is betting that AI agents will increasingly need verified foundations if they are to be useful in software and science without generating errors that are hard to catch later.
That is why the Stacks Project matters beyond academia. If Axiom’s approach works at this scale, it could show that AI systems do not have to improvise from scratch. They can build on checked knowledge that other systems can trust.
Hong went further, openly challenging other coding companies to attempt formalization at the same scale. The challenge is straightforward: if AI is going to produce work people can rely on, speed may not be enough without proof.
