Axiom Math Verifies Stacks Project to Fight AI Slop

Officially launched on November 5, 2026.

Axiom Math has completed formal verification of the Stacks Project, one of the largest and most respected mathematical reference works ever written. The $1.6 billion startup announced Wednesday that its fleet of AI agents successfully translated the project's roughly 7,654 pages into approximately 16 million lines of computer-checked code, creating a verified foundation that AI systems can rely on for software development and scientific research.

The achievement addresses growing concerns about AI-generated errors infiltrating mathematics. With OpenAI alone releasing 719 mathematical manuscripts last month, and computer checks occasionally failing to catch mistakes, the risk of AI slop spreading into foundational mathematics has become a pressing industry concern.

What the Stacks Project Represents

The Stacks Project holds rare status among mathematicians. Columbia University mathematician Peter Woit has stated there is "nothing else really comparable," drawing parallels to the famous Bourbaki books that rebuilt mathematics from its foundations in the 20th century. Johan de Jong, Woit's Columbia colleague, started the open-source reference in 2005, and mathematicians have contributed to it continuously since then.

The project spans college-level algebra through the field's most advanced concepts across algebra, geometry, and number theory. Its theorems and definitions are deeply interconnected, with each result building on those that came before it. This interconnectedness made Axiom initially uncertain whether the verification would succeed.

How Axiom's Agents Preserved Mathematical Integrity

Formal verification translates mathematical proofs into a programming language called Lean, which a proof assistant program then checks line by line. If the proof passes, mathematicians can trust its logical soundness. Engineers use the same technique to confirm chip designs work, while French researchers have used it to catch bugs in benefit calculation software.

"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 team gave its agents a loose structure and allowed them to 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."

Release Date and Availability

Officially announced on November 5, 2026, the verified Stacks Project is now available for mathematicians and AI systems to build upon. The verification fills what Swaminathan describes as 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.

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

Building Verified Foundations for AI's Future

Axiom argues that each verified result becomes a building block for future work. UCLA mathematician and 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 world's code, developers struggle to guarantee their 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 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."

What This Means

The 25-year-old Hong, who dropped out of a Stanford math Ph.D. program and founded the company in March 2025, raised $200 million in Series A funding from Menlo Ventures in March 2026. She argues 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 that's bad engineering choices in the beginning, then it's very hard for them to grow that boundary." Hong has challenged all coding companies to work on formalization at this scale, confident that verified mathematics represents the path forward for trustworthy AI systems.