AI seems to be solving a new math problem every week. Just last month, OpenAI alone published 719 papers claiming to solve some of the field's most difficult problems. Even automated checks can fail. After years of AI-generated junk, it's reasonable to question whether math is next. AxiomMath is betting that math can avoid that outcome—not by slowing down, but by building on a more solid foundation. The $1.6 billion startup aims to create a verified foundation that AI agents can depend on for writing software and, eventually, conducting scientific work. On Wednesday, the company announced it had formally verified the Stacks Project, one of the largest collections of mathematics ever produced by humans.

Mathematicians hold Stacks in unusually high esteem—Columbia mathematician Peter Woit has said there's "nothing else really comparable," likening the project to "the famous Bourbaki books," a series that rebuilt mathematics from its foundations in the 20th century. Woit's Columbia colleague Johan de Jong began the Stacks Project in 2005 as an open-source reference. Mathematicians have contributed to it ever since, expanding results from college-level algebra all the way up to the field's most advanced concepts across algebra, geometry, and number theory. The company's fleet of AI agents converts the library's roughly 7,654 pages into about 16 million lines of computer-checked code.

Formalizing math is a way to ensure the underlying structure is sound. Mathematicians rewrite proofs as code in a programming language called Lean, and a proof assistant program checks the code line by line. If the proof passes, mathematicians can trust that it's logically sound. Engineers use the same concept, called formal verification, to confirm their chip designs work, while researchers in France have used it to catch bugs in software that calculates family benefits. For a library like the Stacks Project, checking each theorem is only part of the job. The theorems and definitions in Stacks are interconnected, and each one builds on those before it. Like a family tree, many results in Stacks trace back to earlier ones. That interconnectedness made Axiom unsure the project would succeed at first. The team had to preserve every connection across about 16 million lines of Lean code.

"[Stacks] is a collection of mathematical results that is the foundation of mathematics. You want [theorems] to be consistent and not, like, paradoxical. You want the definitions to not fight with each other."

The 25-year-old CEO 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. "We were not sure if vibe coding would be able to preserve the beauty of Stacks," Hong said. To accomplish the project, 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 excel at math, an approach Hong said most other verification startups haven't taken. Initially, the team relied on one of its in-house Lean experts to teach the agents a human sense of taste. Over time, Hong said, the agents have developed taste on their own. The result fills one of the biggest gaps in formalized math. "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, Swaminathan said. "Well, now they do."

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

Mathematicians aren't Axiom's only intended audience. Developers have long struggled to guarantee that their code is free of bugs and security vulnerabilities. That problem grows as AI agents write more of the world's code. Axiom is betting that the software of the future will need to rest on 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 and selecting their own tasks—is how Hong expects much of AI's future work to happen. AI agents, she argues, will need a well-built, reusable body of knowledge to avoid producing junk. "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."

Hong is confident enough in that approach to issue a challenge. "I openly challenge all the coding companies to work on formalization at this scale."