AxiomMath verifies the Stacks Project to keep AI slop out of math

What is the Stacks Project?

Johan de Jong, a colleague of Columbia University mathematician Peter Voit, started the project in 2005. It is an open reference work that mathematicians have added to over the years. Voit compared it to the books of Bourbaki—a series that rebuilt mathematics on fundamental foundations in the 20th century—and said the Stacks Project was hard to compare with anything else.

AxiomMath, a $1.6 billion startup, announced on Wednesday that it had completed the project’s formal verification. The company converted the library, about 7,654 pages long, into roughly 16 million lines of Lean code. Its agents worked in parallel.

Formal verification turns a mathematical proof into code. Mathematicians write it in Lean, and a proof assistant checks the code line by line. If it passes, the proof can be considered logically correct. Engineers use the same approach to verify chip designs; researchers in France used it to find errors in software that calculates family benefits.

Why connections between results matter

Checking each theorem separately is not enough: results and definitions in the Stacks Project are connected, and new ones rely on earlier ones. Many, like branches on a family tree, lead back to earlier results.

Those connections initially made AxiomMath question whether it could formalize the whole project. The team had to preserve every connection across a body of about 16 million lines of code. Company head Karina Hong explained that avoiding contradictions between theorems and definitions is especially important in a mathematical foundation like this.

Hong, 25, left Stanford University’s PhD program in mathematics and founded the company in March 2025. In March, AxiomMath raised $200 million in a Series A round led by Menlo Ventures.

To work through the library, the team gave the agents a shared hierarchy but did not spell out each agent’s actions. According to Ashwin Swaminathan, a member of the company’s technical team, the agents found tasks on their own and chose ones they could work on in parallel.

The company also trained its own models in mathematics. Hong noted that most other startups in formal verification had not done this. At first, the agents learned from an AxiomMath Lean specialist, picking up a human sense of mathematical taste. Over time, Hong said, they began developing it on their own.

A foundation for algebraic geometry

The result fills a gap in formalized mathematics: according to Swaminathan, algebraic geometry had remained a largely unexplored area. Researchers who wanted to check new work in the field using Lean previously had no foundation to build on. Now they do.

AxiomMath expects every verified statement to become a building block for future proofs: mathematicians will not have to start from scratch and can instead rely on results that have already been checked. Terence Tao, a UCLA mathematician and Fields Medal winner, put the general principle this way: the more proofs are formalized, the more new proofs can be formalized.

Why verified mathematics matters to software developers

The company sees the project’s audience as extending beyond mathematicians. Developers have long struggled to guarantee that software contains no bugs or vulnerabilities. As AI agents write more and more software, that task is becoming harder.

AxiomMath expects future software to be built on a verified foundation, just as the Stacks Project now rests on formalized results. Swaminathan believes mathematics is well suited to building such foundations, and that the skill can be transferred to other fields: agents can read a company’s code, understand it and build new infrastructure on top of it. Formalization in Lean, he said, provides a base for agents to build on.

Hong expects AI agents to handle more tasks in parallel and choose their own work, as they did while formalizing the Stacks Project. To avoid producing unreliable results, they need a reusable knowledge library on which to build new solutions. If poor engineering decisions are built into the foundation at the outset, expanding it will be difficult. Hong urged companies developing coding tools to take on formalization at this scale.

Dataist's take: The Stacks Project verification shows how formalized mathematics can serve as shared support for future proofs and the work of AI agents. But the result described so far concerns a specific mathematics library and its translation into Lean; the source does not say how far this approach can be applied to other areas of software development.