Artificial intelligence appears to be making inroads into mathematics at a remarkable pace. Just last month, OpenAI published hundreds of manuscripts claiming to offer solutions to some of the discipline's most challenging open problems. Yet even the automated systems used to verify such work have been shown to miss errors. After years of watching AI produce low-quality content across other fields, the question of whether mathematics could be next is no longer entirely hypothetical.

One startup is working to ensure that does not happen - not by putting the brakes on AI-driven mathematical research, but by building a more reliable foundation beneath it. Axiom Math, valued at $1.6 billion, is developing a formally verified mathematical infrastructure that AI agents can use as a trustworthy base when writing software and, over the longer term, conducting scientific research.

Formalizing One of Mathematics' Most Ambitious Projects

On Wednesday, Axiom announced that it had completed the formal verification of the Stacks Project, widely regarded as one of the most extensive bodies of mathematical knowledge ever assembled by human contributors. Among mathematicians, the Stacks Project occupies a position of rare prestige. Columbia University mathematician Peter Woit has described it as having no real equivalent, drawing comparisons to the celebrated Bourbaki series - a landmark 20th-century effort that systematically rebuilt mathematics from its most fundamental principles.

The Stacks Project was launched in 2005 by Columbia mathematician Johan de Jong as an open-source reference work. Since then, mathematicians around the world have contributed to it, expanding its coverage from undergraduate-level algebra through to some of the most advanced ideas in algebra, geometry, and number theory. The project now spans roughly 7,654 pages.

To formally verify this body of work, Axiom deployed a fleet of AI agents that translated the entire library into approximately 16 million lines of computer-checked code.

What Formal Verification Actually Means

Formal verification is the process of converting a mathematical proof into code written in a specialized programming language - in this case, a language called Lean - which is then analyzed line by line by a program known as a proof assistant. If the proof passes this automated inspection, it can be considered logically sound with a high degree of confidence.

The technique is not new to engineering. Chip designers have long used formal verification to confirm that hardware behaves as intended before production. Researchers in France have applied similar methods to identify bugs in software used to calculate government family benefits. What Axiom is doing is applying this level of rigor to a vast and interconnected body of pure mathematics.

That interconnectedness was precisely what made the Stacks Project such a formidable target. Theorems and definitions within the project do not exist in isolation - each one builds on those that came before it, creating a web of dependencies that resembles a complex family tree. Preserving every one of those connections across 16 million lines of Lean code was, by the company's own account, far from a certainty at the outset.

"Things that are big and things that are delicate in life just don't go together," said Axiom CEO Carina Hong. "Stacks is a collection of mathematical results that is the foundation of mathematics. You want theorems to be consistent and not paradoxical. You want the definitions to not fight with each other."

The Team Behind the Effort

Hong, who is 25 years old, left a mathematics PhD program at Stanford University to found Axiom in March 2025. The company raised a $200 million Series A round led by Menlo Ventures earlier this year. Despite her youth and the company's short history, Hong has moved quickly to establish Axiom as a serious player in the formalized mathematics space.

The technical approach Axiom used to verify the Stacks Project involved giving its AI agents a loose organizational structure and allowing them to operate in parallel rather than following a rigid top-down workflow.

"With Stacks, we imposed a hierarchy, but it was not a complete hierarchy of dictating what every single agent was doing," explained 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 developed its own mathematical AI models rather than relying entirely on general-purpose systems - a distinction Hong says sets the company apart from most other startups working in the verification space. Early in the process, the team used one of its in-house Lean experts to help the agents develop a sense of mathematical judgment. Over time, Hong said, the agents have begun to develop that judgment independently.

Filling a Major Gap in Formalized Mathematics

The completion of the Stacks Project verification addresses what Swaminathan described as one of the most significant voids in the existing landscape of 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. Prior to Axiom's work, researchers hoping to verify new results in algebraic geometry using Lean had very little pre-existing formalized material to build upon. That situation has now changed.

Axiom's broader argument is that each formally verified result functions as a reliable building block, enabling future proofs to be constructed on a foundation of already-checked mathematics rather than starting over from first principles each time. Terence Tao, the UCLA mathematician and Fields Medal recipient, has articulated this compounding effect succinctly: "The more formalized proofs you have, the more formalized proofs you can make."

The Broader Ambition: Verified Foundations for Software

Mathematicians are not the only audience Axiom has in mind. Software developers have long grappled with the difficulty of guaranteeing that their code is free of bugs and security vulnerabilities - a challenge that becomes more pressing as AI systems take on a larger share of software development work. Axiom is positioning itself as a provider of the verified infrastructure that future software will need to be built upon.

"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 manner in which Axiom's agents tackled the Stacks Project - dividing work autonomously, running tasks in parallel, and making independent decisions about priorities - reflects Hong's broader vision for how AI agents will function in the future. For that model to work well, she argues, agents will need access to a solid, reusable body of knowledge to prevent the kind of low-quality output that has plagued other areas of AI-generated content.

"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 Axiom's direction to issue a direct challenge to the broader technology industry. "I openly challenge all the coding companies to work on formalization at this scale," she said - a statement that signals the company intends to set the pace in a field it believes will become central to the future of both mathematics and software development.