Axiom Math Formalizes the Entire Stacks Project: 7,654 Pages Turned Into 16 Million Lines of Machine-Checked Lean

Axiom Math, a startup founded by a 25-year-old Stanford math PhD dropout, says its fleet of AI agents has formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. The company announced on Wednesday that it translated the library's roughly 7,654 pages into about 16 million lines of computer-checked Lean code, with every theorem and definition in the original reference preserved.

The Stacks Project is an open-source reference started in 2005 by Columbia mathematician Johan de Jong, built up by contributors from college-level algebra to the most advanced results across algebraic geometry, arithmetic geometry and number theory. Mathematicians treat it with unusual reverence. Columbia's Peter Woit has written that there is "nothing else really comparable," comparing the project to the famous Bourbaki books that rebuilt mathematics from its foundations in the twentieth century.

Formalizing math means rewriting proofs in Lean, a programming language designed for proof assistants, which then check the code line by line. If a proof passes, its logical soundness is no longer a matter of peer review or taste. Engineers already use the same technique, called formal verification, to confirm chip designs work, and the approach is increasingly pitched as an antidote to AI-generated content of dubious correctness.

The scale was the hard part. Theorems in Stacks are deeply interconnected, each building on the ones before it, and Axiom's team had to keep every dependency intact across 16 million lines of code. "Things that are big and things that are delicate in life just don't go together," CEO Carina Hong told TechCrunch. "You want theorems to be consistent and not, like, paradoxical. You want the definitions to not fight with each other."

Rather than micromanaging each agent, the team gave them a loose hierarchy and let them find their own tasks. "The agents were finding tasks for themselves and identified things that they could work on in parallel," said Ashvin Swaminathan, a member of Axiom's technical staff. The company also trains its own models for mathematics rather than relying on general-purpose frontier systems, an approach Hong said most verification startups have not taken.

The result fills what Swaminathan calls a huge black hole in formalized mathematics: algebraic geometry. Researchers who wanted to check new work in the field with Lean previously had almost nothing to build on. "Well, now they do," he said. Fields Medalist Terence Tao has made the general case more simply: "The more formalized proofs you have, the more formalized proofs you can make."

Axiom, founded in March 2025 and valued at $1.6 billion after a $200 million Series A led by Menlo Ventures, is not really selling mathematics. It is selling a verified substrate for AI agents that write software, on the argument that the code of the future will need machine-checkable foundations the way Stacks now provides them for algebraic geometry. Hong is confident enough to issue a dare: "I openly challenge all the coding companies to work on formalization at this scale."