AI agents formally verify a giant math library: Axiom checks the Stacks Project

What's going on

US startup Axiom Math announced on Wednesday that it has formally verified the Stacks Project. That means every theorem and definition in one of the most extensive math collections humans have ever written has been checked for logical correctness by a computer. The work was done by a fleet of AI agents, AI programs that independently pick up and work through subtasks. They translated around 7,654 pages into roughly 16 million lines of code.

Axiom, valued at around $1.6 billion according to TechCrunch, pitches the project as an antidote to "AI slop", the term for low-quality, mass-produced AI content. The backdrop: AI systems now deliver supposed solutions to math problems almost weekly. TechCrunch notes that OpenAI published 719 manuscripts last month with claimed solutions to some of the field's hardest problems. Who's supposed to check all that?

What the Stacks Project is

Mathematician Johan de Jong started the Stacks Project at Columbia University in 2005 as a freely accessible reference work. Many mathematicians have contributed since, covering everything from first-year algebra to the most advanced ideas in algebra, geometry and number theory. Columbia mathematician Peter Woit told TechCrunch there's "nothing really comparable" and likened it to the famous Bourbaki books, a series in which a group of French mathematicians rebuilt mathematics from the ground up in the 20th century.

The tricky part: the content is tightly interwoven. Like a family tree, almost every result builds on earlier definitions and theorems. Every one of those connections had to survive the translation across 16 million lines of code.

"Things that are big and things that are delicate just don't go together in life," Axiom CEO Carina Hong told TechCrunch. "You want the theorems to be consistent and not paradoxical. You want the definitions to not fight each other."

How formal verification works

Formalization means translating a mathematical proof into the programming language Lean. A proof assistant, a program that checks every logical step like an extremely pedantic proofreader, then verifies it line by line. If the code passes, mathematicians can be sure the proof is logically sound. Engineers use the same principle, called formal verification, to validate chip designs; according to TechCrunch, it was even used in France to find bugs in software that calculates family benefits.

Axiom itself wasn't sure it would work. "We didn't know whether vibe coding could preserve the beauty of Stacks," Hong said. Vibe coding means programming by letting an AI write code largely on its own.

An agent swarm with a loose hierarchy

The team gave the agents only a rough structure and let them work in parallel. "We imposed a hierarchy, but not a complete one that dictated what every single agent should do," explains Ashvin Swaminathan from the technical team. "The agents found tasks for themselves and figured out what they could work on in parallel."

Axiom also trained its own math-specialized models, a step Hong says most other verification startups haven't taken. Early on, an in-house Lean expert gave the agents a human sense of good style; by now, the agents have developed that sense themselves (company claim).

Swaminathan says the result closes a big gap: "If you look at what's been formalized in mathematics, there's this huge black hole. And that's algebraic geometry." Anyone wanting to check new work in this field with Lean had almost nothing to build on until now. "Now they do."

Backstory: the "enormous theorem" in 24 days

The Stacks announcement comes just days after an even more spectacular project. On October 27, according to Unite.AI, Axiom published what it calls the first fully machine-checked proof of the classification of finite simple groups. The theorem describes the building blocks of all finite groups; the original proof spans around 15,000 pages in more than 500 papers by about 100 mathematicians and is nicknamed "the enormous theorem".

Axiom says the work took 24 days: starting October 2, swarms of dozens of agents worked through 108 milestones and around 380 smaller tasks, coordinated via GitHub issues and Slack. It wasn't smooth sailing. Agents assumed prerequisites instead of proving them, and the team deleted tens of thousands of lines and replanned. Checking by Lean also became a bottleneck, because the agents produced proofs faster than Lean could verify them.

Particularly interesting: during translation, the agents ran into 34 notable discrepancies in the published literature, mostly typos, incorrect tables or forgotten assumptions. In a lemma by Aschbacher and Smith, they found a counterexample involving the group SL₂(5). For the "Unbalanced Group Theorem", they discovered counterexamples to a claim in John Walter's 1986 paper; the gap was closed with what Axiom says is a new theorem proved by its AxiomProver system. The theorem itself was not disproved. The code is on GitHub under the Apache 2.0 license; Axiom plans to work through the list of errors with group theorists such as Richard Lyons and Ronald Solomon.

The company and its bet

Carina Hong, 25, dropped out of a math PhD at Stanford and founded Axiom in March 2025. In March of this year, the company raised $200 million in a Series A led by Menlo Ventures. Its real target audience isn't just mathematicians: Axiom is betting that software, increasingly written by AI agents, will need to stand on verified foundations to rule out bugs and security holes.

"Math is the field where you start building things like this, and it's a transferable skill," says Swaminathan. "Our Lean formalization is now the substrate agents can build on." Fields Medalist Terence Tao summed up the principle: "The more formalized proofs you have, the more formalized proofs you can create." Hong is confident: "I openly challenge all the coding companies to work on formalization at this scale."

The bigger picture

Formal verification is one of the few ways to check AI output truly reliably: not through trust, but through mechanical checking. Agents pulling off in weeks what human teams would need years for is a clear step forward, and mathematicians in algebraic geometry get a usable foundation.

Caveats remain. So far, the claims come from the company itself; independent review of the 16 million lines by the research community is still pending. The sources don't say whether the Stacks code is openly available like the group proof. Formal verification also only guarantees that the proofs match the formalized statements; whether those statements capture exactly what the original authors meant is a separate question. And whether the approach carries over to general software development, as Axiom hopes, is so far a bet, not a proven fact.