AxiomMath Formalizes the Stacks Project to Give AI a Verified Math Foundation

Each week brings fresh announcements of AI systems solving mathematical problems. OpenAI published 719 manuscripts last month alone, each purporting to address some of mathematics' most difficult open questions. Yet automated verification itself can fail. Given the prevalence of AI-generated content of questionable quality across other fields, mathematics faces a similar risk. AxiomMath, valued at $1.6 billion, is pursuing a different strategy: rather than restraining progress, the company aims to construct a rigorously verified base upon which AI agents can construct software and conduct scientific research.

This week, AxiomMath announced the formal verification of the Stacks Project, among the most comprehensive mathematical works ever assembled by human mathematicians. The project commands exceptional respect within the mathematical community—Peter Woit, a mathematician at Columbia University, has stated there is "nothing else really comparable," drawing a parallel to "the famous Bourbaki books," the influential 20th-century effort to reconstruct mathematics from foundational principles.

Johan de Jong, also at Columbia, initiated the Stacks Project in 2005 as a collaborative open-source resource. Since its inception, mathematicians worldwide have contributed, expanding the collection from introductory algebra through the most sophisticated developments in algebra, geometry, and number theory. AxiomMath's AI agents have converted the project's approximately 7,654 pages into roughly 16 million lines of machine-verifiable code.

How Formal Verification Works

Formal verification ensures the logical integrity of mathematical arguments. Mathematicians translate proofs into Lean, a programming language designed for this purpose, and a proof assistant then validates every line. Once a proof passes verification, its logical correctness is guaranteed. This same technique allows engineers to validate chip designs and has helped researchers in France identify bugs in software used to calculate social benefits.

For a resource as extensive as the Stacks Project, verification extends beyond individual theorems. Within Stacks, theorems and definitions form an intricate web, with each result depending on prior ones. Similar to genealogical connections, many findings in Stacks ultimately trace back to earlier foundational results. This interconnectedness initially raised questions about whether the verification effort could succeed. The team needed to maintain every relationship across all 16 million lines of Lean code.

"Things that are big and things that are delicate in life just don't go together," AxiomMath 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."

Building the Verification at Scale

Hong, 25 years old, departed from a Stanford mathematics Ph.D. program to establish AxiomMath in March 2025. The company closed a Series A funding round in March, raising $200 million with Menlo Ventures as lead investor.

To accomplish the Stacks verification, the team structured its agents loosely and allowed them to operate concurrently. "With Stacks, we imposed a hierarchy… [but] it was not, like, a complete hierarchy of dictating what every single agent was doing," explained Ashvin Swaminathan, a technical staff member at AxiomMath. "The agents were finding tasks for themselves and identified things that they could work on in parallel."

AxiomMath also developed proprietary models specialized in mathematical reasoning—a strategy Hong noted that competing verification companies have not adopted. Initially, an in-house Lean specialist helped train the agents to develop mathematical judgment. Over time, according to Hong, the agents have developed this capability independently.

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

Filling a Critical Gap

The project addresses a significant void 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. Researchers seeking to verify new algebraic geometry results using Lean previously had minimal existing formalized work to build upon. "Well, now they do."

AxiomMath contends that each verified result becomes a foundation for subsequent proofs, allowing future work to build on established, checked mathematics rather than beginning anew. Terence Tao, the UCLA mathematician and Fields Medal recipient, has articulated this principle concisely: "The more formalized proofs you have, the more formalized proofs you can make."

Beyond Mathematics

AxiomMath's vision extends beyond the mathematical community. Software developers have long struggled to ensure their code contains no defects or security vulnerabilities—a challenge that intensifies as AI agents generate increasing portions of the world's software. AxiomMath is positioning verified foundations as essential infrastructure for the software era ahead, just as Stacks now provides verified mathematics.

"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."

Hong envisions the parallel, self-directed approach her agents used to formalize Stacks as a model for future AI work. She argues that AI systems require well-constructed, reusable knowledge bases to prevent the generation of unreliable outputs.

"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 has publicly challenged the software industry to match her company's ambition. "I openly challenge all the coding companies to work on formalization at this scale."