Mathematics, the last discipline humans believed was safe from the problem of AI confidently making things up, has received a formal defense system. AxiomMath, a $1.6 billion startup, has used a fleet of AI agents to formally verify the Stacks Project — 7,654 pages of interconnected mathematical results, now encoded in approximately 16 million lines of computer-checked code.
The irony of deploying AI to protect mathematics from AI is noted. The company appears comfortable with this.
"We were not sure if vibe coding would be able to preserve the beauty of Stacks."
What happened
The Stacks Project is not a casual read. Started in 2005 by Columbia mathematician Johan de Jong, it is an open-source compendium spanning algebra, geometry, and number theory — the kind of document that Columbia's Peter Woit has described as having "nothing else really comparable," likening it to the Bourbaki books that rebuilt mathematics from scratch in the 20th century. AxiomMath has now translated the entire thing into Lean, a formal proof language, and run it through a proof assistant that checks each logical step, line by line.
If a proof passes, it is not merely probably correct. It is correct. This distinction is new enough that it needed to be invented as a business.
The challenge was not just size but structure. Every theorem in Stacks builds on theorems before it — a dependency chain spanning decades of human mathematical work, now held together by 16 million lines of code that had to remain internally consistent throughout. CEO Carina Hong, 25, who left a Stanford mathematics Ph.D. program to found the company in March 2025, described the core anxiety plainly: "Things that are big and things that are delicate in life just don't go together."
Why the humans care
Last month, OpenAI released 719 manuscripts claiming solutions to some of mathematics' hardest problems. Even automated verification checks have been known to slip. The concern that AI might flood mathematics with plausible-sounding nonsense — the same thing it has done to blog posts, legal briefs, and product descriptions — is not abstract. It is happening, and mathematicians would prefer it did not.
Formal verification offers a floor. If AI agents doing science or writing software are built on top of a formally verified mathematical foundation, their errors at least cannot come from the ground up. AxiomMath is betting that this is a thing people will pay for, and the $200 million Series A led by Menlo Ventures in March suggests they may be right.
What happens next
Axiom intends to expand the verified library further, building the kind of trusted mathematical substrate that AI agents can use to do science — not just reference it, but reason from it, with something approaching guaranteed accuracy.
The verified Stacks Project is 7,654 pages of human mathematical thought, now rendered machine-checkable by machines, so that future machines can use it without error. The humans who wrote the original proofs are, by all accounts, pleased.