Startup uses AI to double-check a giant library of math proofs

A startup called Axiom Math says its AI agents have checked an entire giant library of math proofs, line by line, using a program that does not take anything on faith. The library is the Stacks Project. Axiom announced the result on Wednesday. The pitch is simple: as AI produces more unchecked work, the answer is to verify it.

What Axiom did

The Stacks Project is an open source reference that Columbia mathematician Johan de Jong started in 2005. Mathematicians have added to it ever since, from college-level algebra up to some of the field's most advanced ideas. Axiom's AI agents translated its roughly 7,654 pages into about 16 million lines of computer-checked code.

How the checking works

Mathematicians rewrite a proof as code in a programming language called Lean. A program called a proof assistant then checks the code line by line. If the proof passes, it is logically sound. This idea is called formal verification.

The results in Stacks build on one another, much like a family tree. Axiom's team had to keep every connection intact across all that code. CEO Carina Hong said the team was not sure at first that the project would work.

Why it matters beyond math

The material notes that engineers already use formal verification to confirm that chip designs work. Researchers in France have used it to catch bugs in software that calculates family benefits. Developers have long struggled to guarantee that code is free of bugs and security holes, and that problem grows as AI agents write more of the world's code.

Axiom is betting that future software will need to rest on verified foundations, the way Stacks now does. The company says each verified result becomes a building block that later proofs can use instead of starting over.

The company and its claims

Axiom is valued at $1.6 billion. It raised a $200 million Series A in March, led by Menlo Ventures. Hong, who is 25, dropped out of a Stanford math PhD program and founded the company in March 2025. She said Axiom trained its own math models, which she says most other verification startups have not done.

The agents worked in parallel with a loose structure and picked many of their own tasks. Axiom says the result fills a big gap in checked math, in an area called algebraic geometry.

What is not known yet

The material gives no timeline for applying this to everyday software. Axiom's claim that its approach transfers from math to code is a bet, not a proven result. Hong has also challenged other coding companies to take on formalization at this scale.