Axiom Math Turns 7,654 Pages of Math Into 16 Million Lines of Verified Code

AxiomMath announced on Wednesday that it has formally verified the Stacks Project, translating roughly 7,654 pages of human-written mathematics into about 16 million lines of computer-checked code.

The $1.6B startup wants math to escape the flood of AI slop that has hit other fields. Last month, OpenAI alone released 719 manuscripts claiming solutions to some of math's hardest problems, and even computer checks can slip. Axiom's answer isn't to slow down. It's to build a verified foundation that AI agents can rely on to write software and, eventually, do science.

Why the Stacks Project matters

Mathematicians hold the Stacks Project in rare regard. Columbia mathematician Peter Woit has claimed there's "nothing else really comparable," comparing the project to "the famous Bourbaki books," the 20th-century series that rebuilt math from its foundations.

Woit's Columbia colleague Johan de Jong started Stacks in 2005 as an open-source reference. Contributors have built it out ever since, from college-level algebra up to the field's most advanced ideas across algebra, geometry and number theory.

Formalizing it means rewriting proofs as code in a programming language called Lean. A proof assistant then checks the code line by line. If the proof passes, mathematicians can trust it's logically sound. Engineers use the same idea — formal verification — to confirm chip designs, and researchers in France have used it to catch bugs in software that calculates family benefits.

How did the agents pull it off?

The hard part wasn't just checking theorems. Stacks' theorems and definitions are interconnected, each one building on the ones before it, like a family tree. Axiom's team had to keep every connection intact across roughly 16 million lines of Lean code.

"Things that are big and things that are delicate in life just don't go together," Axiom CEO Carina Hong told TechCrunch. "You want [theorems] to be consistent and not, like, paradoxical. You want the definitions to not fight with each other."

Hong, 25, dropped out of a Stanford math Ph.D. program and founded the company in March 2025. In March, Axiom raised a $200 million Series A led by Menlo Ventures.

The team gave its agents a loose structure and let them run in parallel. "With Stacks, we imposed a hierarchy… [but] it was not, like, a complete hierarchy of dictating what every single agent was doing," said Ashvin Swaminathan, a member of Axiom's technical staff. "The agents were finding tasks for themselves and identified things that they could work on in parallel."

Axiom also trained its own models to be good at math — an approach Hong said most other verification startups haven't taken. At first, one in-house Lean expert taught the agents a human sense of taste. Over time, Hong said, the agents picked up taste on their own.

"We were not sure if vibe coding would be able to preserve the beauty of Stacks," Hong said.

What does this change for math?

The result fills one of the biggest gaps 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," Swaminathan said. Until now, researchers who wanted to check new work in algebraic geometry with Lean had little to build on. "Well, now they do."

Axiom argues each verified result becomes a building block, so future proofs can lean on checked math instead of starting from scratch. UCLA mathematician and Fields Medal winner Terence Tao has made the case simply: "The more formalized proofs you have, the more formalized proofs you can make."

The bigger bet: verified software

Mathematicians aren't Axiom's only audience. Developers have long struggled to guarantee code is free of bugs and security holes, and that problem grows as AI agents write more of the world's code. Axiom is betting the software of the future will need verified foundations, the way Stacks now does.

"We believe that mathematics is the domain where you start building these things, and that it's a transferable skill," Swaminathan said. "Agents can read our code, understand it, and build new infrastructure on top of it. Our Lean formalization is now the substrate that agents can build upon."

The way Axiom's agents built Stacks — working in parallel, picking their own tasks — is how Hong expects much of AI's future work to happen. Agents, she argues, will need a well-built, reusable body of knowledge to keep from producing slop.

"You want [agents] to have a reusable library for them to build on and keep pushing the frontier," Hong said. "If you slop drop in a way that's bad engineering choices in the beginning, then it's very hard for them to grow that boundary."

She's confident enough to issue a dare: "I openly challenge all the coding companies to work on formalization at this scale."

By Grace Kim