Axiom Math Used Agents to Verify 16 Million Lines of Lean Code, Closing a Gap in Formal Mathematics

When AI "solves" a new math problem every week, a reasonable question arises: who checks all of it? Last month alone, OpenAI released 719 manuscripts with claimed solutions to hard problems. Reading them all by hand is impossible, and errors slip through even with machine checks. Axiom Math, a startup valued at $1.6 billion, proposes a different path: not slowing down, but building on a verified foundation.

What Exactly Was Done

On Wednesday the company announced that it had formally verified the Stacks Project, one of the largest collections of human mathematics in history. It was started in 2005 by Johan de Jong of Columbia University as an open reference. Today it contains about 7,654 pages: from undergraduate algebra to cutting-edge ideas in algebraic geometry and number theory.

Axiom's agents rewrote all of this as roughly 16 million lines of code in the Lean language. Then a program called a proof assistant checked the code line by line. If the check passes, the proof is logically correct, and there is no need to take the author's word for it.

Why It Is Harder Than It Looks

Verifying each theorem individually is only half the job. Results in the Stacks Project are linked like a family tree: each relies on earlier ones. If a definition "drifts" somewhere, everything above it collapses. So the team had to preserve all the connections across 16 million lines. CEO Carina Hong herself admits she was initially unsure of success: large and fragile do not go well together.

The architecture was this: a soft hierarchy on top, but no rigid task allocation. Agents found things to work on themselves and worked in parallel. Axiom also trained its own models for mathematics, which, according to Hong, most competitors in verification do not do. At first, an in-house Lean expert instilled "taste" in the agents, an understanding of what good code should look like. Over time, Hong says, they learned to manage on their own.

Why Developers Should Care

The practical point is not algebraic geometry itself. Formal verification has long been used where errors are costly: chip verification, and French researchers used it to find bugs in software that calculates family benefits. The problem is that agents write more and more code, while guarantees against bugs and security holes are not increasing.

Axiom's bet: mathematics is a proving ground where this skill is honed and then transferred to software. Agents can read a ready-made Lean library and build new things on it without starting from scratch. Terence Tao states the general principle this way: the more formalized proofs there are, the more new ones can be built.

Limitations

For now this is the company's own claim, and the article contains no independent assessment of the result. Transferring the skill from mathematics to production code is a hypothesis, not a proven fact. Real software depends on the environment, dependencies, and informal requirements that do not formalize as cleanly as theorems. Hong's challenge to all companies writing code to undertake formalization at this scale sounds bold, but so far it is more marketing.

What to Do in Practice

If you are building agentic systems for code, take a look at Lean and the idea of verifiable artifacts: have the agent output not only code but also something that can be checked automatically. For product teams the takeaway is simpler: "AI wrote it" and "AI wrote it and it is proven" will soon become two different quality categories. Those working in critical areas such as finance, medicine, and security should keep this shift on their radar now.