Verifying Mathematical Foundations
As AI models increasingly generate solutions to complex mathematical problems, concerns regarding the accuracy of these outputs have grown. Axiom Math, a startup valued at $1.6 billion, aims to address this by building a verified foundation that AI agents can utilize for software development and scientific research.
The company recently announced the formal verification of the Stacks Project, an extensive open-source reference for mathematics initiated by Johan de Jong in 2005. The project covers a wide range of advanced topics, including algebra, geometry, and number theory.
Axiom’s AI agents translated approximately 7,654 pages of the Stacks Project into 16 million lines of code written in Lean, a programming language used for formal verification. This process allows a proof assistant program to check the logic of mathematical proofs line by line, ensuring they are sound.
Scaling Formalization with AI
The project required maintaining the integrity of interconnected theorems across the entire library. Axiom utilized a parallelized approach where AI agents identified and executed tasks independently within a loose hierarchy. The company also trained its own models to develop a sense of mathematical taste, improving the efficiency and accuracy of the formalization process.
By formalizing this body of work, Axiom provides a resource for researchers in fields like algebraic geometry to build upon existing verified results. This modular approach is intended to allow future proofs to rely on checked foundations rather than starting from scratch.
Future Applications in Software
Beyond mathematics, Axiom views formal verification as a critical tool for software engineering. As AI agents take on more coding tasks, the company argues that verified foundations will be essential to prevent errors and security vulnerabilities. Axiom intends for its Lean formalization to serve as a substrate for future AI-driven infrastructure development.
Axiom CEO Carina Hong, who founded the company in 2025, emphasizes that providing agents with a reusable, verified library is necessary to maintain high standards in AI-generated work.
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 the ones before it. Like a family tree, many results in Stacks trace back to the ones that came before it.
That interconnectedness made Axiom unsure the project would work at first. The team had to keep every connection intact across about 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. “[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 PhD 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 pull off 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 be good at math, an approach Hong said most other verification startups haven’t taken. At first, 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 picked up 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 argues that each verified result becomes a building block, so future proofs can lean 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 holes. 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 picking 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 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.”
Hong is confident enough in that approach to issue a dare. “I openly challenge all the coding companies to work on formalization at this scale.”
