Artificial intelligence seems to be conquering new mathematical challenges every week. Just last month, OpenAI presented 719 papers claiming solutions to some of the most difficult problems in the field. However, even automated verifications can contain errors. After years of encountering unreliable AI outputs, it’s reasonable to question whether mathematics will suffer a similar fate.
Axiom Math believes that math can avoid this outcome, not by slowing down, but by establishing a more secure foundation. The $1.6 billion startup aims to construct a verified bedrock that AI agents can depend on for software development and, eventually, scientific discovery.
On Wednesday, the company announced the formal verification of the Stacks Project, which is recognized as one of the most extensive collections of human-written mathematics. Mathematicians often hold Stacks in exceptionally high regard; Peter Woit, a mathematician at Columbia, has stated there’s “nothing else truly comparable,” drawing parallels to “the famous Bourbaki books,” a series that rebuilt mathematics from its core principles in the 20th century.
Johan de Jong, Woit’s colleague at Columbia, launched the Stacks Project in 2005 as an open-source reference. Since then, mathematicians have continuously contributed to it, expanding its content from college-level algebra to the field’s most advanced concepts across algebra, geometry, and number theory.
Axiom’s network of AI agents converts the library’s approximately 7,654 pages into around 16 million lines of computer-checked code.
Formalizing mathematics ensures the underlying structure is robust. This involves mathematicians rewriting proofs as code in a programming language called Lean, and then a proof assistant program verifies the code line by line. If a proof passes this check, its logical soundness can be trusted by mathematicians.
Engineers utilize this same concept, known as formal verification, to validate their chip designs, while French researchers have applied it to identify bugs in software that calculates family benefits.
For a vast collection like the Stacks Project, merely checking individual theorems is insufficient. The theorems and definitions within Stacks are intricately linked, with each building upon preceding ones. Much like a genealogical tree, many results in Stacks can be traced back to earlier foundational concepts.
This intricate interconnectedness initially caused Axiom to doubt the project’s feasibility. The team faced the challenge of maintaining every single connection across approximately 16 million lines of Lean code.
“In life, things that are grand and things that are delicate typically don’t coexist,” Axiom CEO Carina Hong explained to TechCrunch. “[Stacks] is a compilation of mathematical findings that forms the very foundation of mathematics. You need [theorems] to be consistent and free from paradoxes. You want the definitions to be in harmony, not conflict.”
The 25-year-old CEO, who left a Stanford math PhD program, established the company in March 2025. That same month, Axiom secured a $200 million Series A funding round led by Menlo Ventures.
“We had doubts whether our ‘vibe coding’ approach could genuinely preserve the elegance of Stacks,” Hong admitted.
To accomplish the project, the team implemented a flexible structure for its agents, allowing them to operate in parallel. “For Stacks, we established a hierarchy… [but] it wasn’t a rigid hierarchy dictating every action of each agent,” stated Ashvin Swaminathan, a member of Axiom’s technical staff. “The agents autonomously identified tasks and determined what they could work on concurrently.”
Axiom also developed and trained its own models specifically to excel in mathematics, an approach Hong notes most other verification startups have not adopted. Initially, the team relied on an in-house Lean expert to impart a human-like sense of discernment to the agents. Over time, Hong observed that the agents independently acquired this ‘taste’.
This accomplishment addresses one of the most significant gaps in formalized mathematics. “When you examine what has been formalized in mathematics, there’s this enormous void. That void encompasses algebraic geometry,” Swaminathan explained.
Previously, researchers seeking to verify new work in algebraic geometry using Lean had very few existing resources to build upon, Swaminathan added. “Now, they do.”
Axiom contends that each verified result serves as a foundational building block, enabling future proofs to rely on rigorously checked mathematics rather than starting from scratch. Terence Tao, the UCLA mathematician and Fields Medal laureate, has articulated this principle more succinctly: “The more formalized proofs you possess, the more formalized proofs you are capable of creating.”
Axiom’s intended audience extends beyond mathematicians. Developers have long struggled to ensure their code is free from bugs and security vulnerabilities. This challenge intensifies as AI agents generate an increasing amount of the world’s software.
Axiom is banking on the idea that future software will necessitate verified foundations, mirroring the rigorous verification now applied to Stacks.
“We believe mathematics is the ideal domain to commence building these systems, and that this is a transferable skill,” Swaminathan remarked. “Agents can interpret our code, comprehend it, and construct new infrastructure upon it. Our Lean formalization now provides the fundamental substrate that agents can build upon.”
The parallel, self-directed working method employed by Axiom’s agents in building Stacks is how Hong envisions much of AI’s future work unfolding. She argues that AI agents will require a robust, reusable body of knowledge to avoid producing inferior results.
“You want [agents] to possess a reusable library as a basis for their development and to continually push the boundaries,” Hong explained. “If you ‘slop drop’ due to poor engineering decisions at the outset, it becomes exceedingly difficult for them to expand that frontier.”
Hong is so confident in this strategy that she has issued a challenge. “I openly dare all coding companies to undertake formalization at this magnitude.”