Axiom Math uses AI agents to formally verify the entire Stacks Project in Lean

What the Stacks Project is

The Stacks Project is an open-source reference work in algebraic geometry started by Columbia University mathematician Johan de Jong in 2005. Mathematicians have contributed to it continuously ever since, building out results from college-level algebra all the way up to the fields most advanced ideas across algebra, geometry and number theory.

Columbia mathematician Peter Woit has said there is "nothing else really comparable" to Stacks, comparing it to the famous Bourbaki books that rebuilt mathematics from its foundations in the 20th century. The project spans roughly 7,654 pages of densely interconnected theorems and definitions, each building on those that came before it.

That interconnectedness made Axiom unsure the project would work at first. "Things that are big and things that are delicate in life just dont go together," 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."

How Axioms agents did the work

Formal verification translates mathematical proofs into a programming language called Lean. A program called a proof assistant then checks the code line by line. If the proof passes, mathematicians can trust that it is logically sound. Engineers use the same idea to confirm chip designs work, while French researchers have used it to catch bugs in benefit calculation software.

Axiom deployed a fleet of AI agents that translated the entire Stacks Project into approximately 16 million lines of Lean code. Rather than dictating every step, the team gave the agents a loose hierarchy and let them find work in parallel.

The parallel approach distinguishes Axiom from traditional formal verification projects, which typically require mathematicians to write Lean code by hand. Previous efforts to formalize portions of the Stacks Project had made only limited progress because of the sheer scale. Axioms agents automated the translation while preserving the logical connections between interdependent theorems.

"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 Axioms technical staff. "The agents were finding tasks for themselves and identified things that they could work on in parallel."

The company also trained its own models specifically to excel at mathematics, an approach Hong said most other verification startups have not taken. Initially, one of Axioms in-house Lean experts taught the agents a human sense of mathematical taste. Over time, the agents developed their own judgment.

The result fills what Swaminathan calls a "huge black hole" in formalized mathematics covering algebraic geometry, an area where researchers previously had little verified foundation to work from when using Lean. "Well, now they do," he said.

Why verified math matters for AI

The announcement comes as AI systems produce more mathematical output than ever. Last month, OpenAI alone released 719 mathematical manuscripts claiming solutions to some of the fields hardest problems. But even the computer checks meant to confirm those results can slip, and the risk of AI-generated errors infiltrating foundational mathematics has become a pressing concern.

The concern is not academic. OpenAI revealed last month that its own automated checks sometimes miss errors in AI-generated mathematical manuscripts. The company released 719 manuscripts in October 2026 claiming solutions to some of the fields hardest problems, but even the verification systems designed to catch mistakes can slip. Axioms approach addresses this by building from verified foundations upward rather than attempting to check each new claim in isolation.

Axiom argues that each verified result becomes a building block for future work. Fields Medal winner Terence Tao has made the case simply: "The more formalized proofs you have, the more formalized proofs you can make."

Beyond pure mathematics, Axiom is targeting software development. As AI agents write increasing amounts of the worlds code, developers struggle to guarantee that output is free of bugs and security vulnerabilities. The company believes future software will need to rest on verified foundations similar to what the Stacks Project now provides.

"We believe that mathematics is the domain where you start building these things and that its 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 company behind the verification

Axiom Math was founded in March 2025 by Carina Hong, who dropped out of a Stanford math PhD program at age 24. The company raised a $200 million Series A led by Menlo Ventures at a $1.6 billion valuation. Hongs vision is that AI agents will need a well-built, reusable body of knowledge to avoid producing unreliable output.

"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 thats bad engineering choices in the beginning, then its very hard for them to grow that boundary."

Hong issued an open challenge to coding companies: "I openly challenge all the coding companies to work on formalization at this scale."

Axioms approach sets it apart from other verification startups by training its own models for mathematical reasoning rather than relying on third-party models. The company now plans to use the verified Stacks Project as a foundation for larger ambitions, including verified software infrastructure that AI agents can build on without introducing logical errors.