Axiom Math's agents turned 7,654 pages of human math into 16 million lines of checked Lean

Formal verification just got a very large new library. Axiom Math says its AI agents have finished a formal verification of the Stacks Project, one of the biggest bodies of mathematics humans have ever written, Aditya Mehta reports for TechCrunch.

What Stacks is

The project dates to 2005, when Columbia mathematician Johan de Jong launched it as an open reference. Contributors have built it out ever since, from college algebra up to the most advanced ideas in algebra, geometry and number theory. Mathematicians hold it in unusual esteem; Columbia's Peter Woit has compared it to the Bourbaki books that rebuilt math from its foundations.

Axiom's agents turned its roughly 7,654 pages into some 16 million lines of Lean, the language mathematicians use to write proofs as code. A proof assistant then checks every line. If a proof passes, its logic holds.

Why this was hard

Checking theorems one at a time is the easy half. Results in Stacks depend on earlier ones like a family tree, so every link had to survive the translation intact. CEO Carina Hong said the team wasn't sure "vibe coding" could keep the structure consistent, with definitions that don't contradict each other.

The method is the interesting part for developers. Axiom set a loose hierarchy and let agents run in parallel, choosing their own tasks rather than being told what to do. It also trained its own math models, which Hong says most verification startups haven't done. A human Lean expert first taught the agents a sense of taste; over time, she says, they developed it themselves.

Why it matters beyond math

Algebraic geometry has been a big hole in formalized math. Researchers who wanted to check new work there with Lean had little to build on. Now they have a base, and as Terence Tao has put it, more formal proofs make more formal proofs possible.

Axiom, valued at $1.6 billion after a $200 million Series A in March, says the real target is software. With agents producing a growing share of code, guaranteeing it's free of bugs and security holes gets harder, and Axiom argues future software should rest on verified foundations. Hong even dared coding companies to attempt formalization at this scale.

The caveat: Axiom's claims about agent "taste" come from Axiom, and a verified library is only as useful as the people and agents who build on it. But a 16-million-line Lean library you can trust beats another leaderboard number.

Scoreboard update: AI +1. Agents formally verify a landmark library of human mathematics.

Stay undead.