AxiomMath Turns the Math Slop Problem into a Verified Foundation for AI

AI has been cracking math problems faster than ever, with OpenAI alone publishing 719 new manuscripts last month. Yet the rush has left a trail of sloppy proofs that even computer checks can miss. AxiomMath, a $1.6 billion startup, is betting that mathematics can stay clean by standing on firmer ground.

The company’s first milestone was the formal verification of the Stacks Project, a massive open‑source reference that spans 7,654 pages of advanced algebra, geometry, and number theory. Axiom’s fleet of AI agents translated the text into about 16 million lines of Lean code, a programming language that lets a proof assistant check every logical step.

To keep the web of definitions and theorems intact, the team let the agents work in parallel under a loose hierarchy, letting each find its own tasks while preserving the overall structure. The result fills a huge black hole in formalized math. Until now, researchers in algebraic geometry had little Lean infrastructure to build on.

With the Stacks Project verified, new proofs can lean on a solid, checked foundation.

As Fields Medalist Terence Tao put it, “The more formalized proofs you have, the more formalized proofs you can make.”Axiom’s vision extends beyond pure math.

Developers have long struggled to guarantee bug‑free code, a challenge that will grow as AI writes more software.

By turning verified math into a reusable library, Axiom believes future AI agents can build reliable software and even conduct science without producing slop.

Our read: if Axiom’s approach scales, it could set a new standard for AI reliability, making verified mathematics the bedrock of tomorrow’s technology.