Axiom Math announced on Wednesday that it has formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. According to TechCrunch AI, the $1.6 billion startup’s AI agents turned roughly 7,654 pages into about 16 million lines of computer-checked code. It’s a big claim, and it comes as the industry starts asking whether math is about to get its own slop problem.
The quick read
- What happened: Axiom’s agents converted the Stacks Project into Lean, a programming language used to write proofs that software can check.
- Why mathematicians care: The work fills what Axiom calls a major gap in formalized math, especially in algebraic geometry.
- Why everyone else should care: Axiom says the same verified foundations can support AI-written software and, eventually, AI-driven science.
- What to watch: Whether outside mathematicians build on this library, and whether coding AI companies take up CEO Carina Hong’s public challenge.
Why Stacks is a serious test
Columbia mathematician Johan de Jong started the Stacks Project in 2005 as an open source reference. Contributors have since built it out from college-level algebra to the most advanced ideas in algebra, geometry, and number theory. His Columbia colleague Peter Woit has said there’s “nothing else really comparable,” comparing it to “the famous Bourbaki books.”
The size wasn’t the only problem. Stacks works like a family tree, with results depending on the ones before them, so one bad translation could damage everything built on top of it. Axiom had to keep those connections intact across the whole project.
“Things that are big and things that are delicate in life just don’t go together,” Hong told TechCrunch. She also admitted the team doubted the approach at first: “We were not sure if vibe coding would be able to preserve the beauty of Stacks.”
How the agents did it
Formal verification means rewriting a proof as code, then having a program called a proof assistant check it line by line. Chip engineers use the same idea to confirm their designs work. Researchers in France have used it to catch bugs in software that calculates family benefits.
Axiom’s setup had a few notable pieces:
- Loose hierarchy: The team imposed some structure but didn’t dictate each agent’s work. Technical staff member Ashvin Swaminathan said the agents were “finding tasks for themselves” and spotting work they could do in parallel.
- Custom models: Axiom trained its own models to be good at math, an approach Hong said most other verification startups haven’t taken.
- Human taste, at first: An in-house Lean expert initially taught the agents a human sense of taste. Hong says they’ve since picked it up on their own.
Why this matters beyond math
What stands out here is the timing. Last month, OpenAI released 719 manuscripts claiming solutions to some of the field’s hardest problems, and even the computer checks meant to confirm results like these can slip. AI can now produce math faster than people can comfortably review it.
Axiom’s answer is a reusable base of checked results, so future proofs don’t start from scratch. Until now, Swaminathan said, researchers who wanted to check new algebraic geometry work in Lean had little to build on. Terence Tao, the UCLA mathematician and Fields Medal winner, has made the general case: “The more formalized proofs you have, the more formalized proofs you can make.”
The commercial bet is on software. Developers have long struggled to guarantee their code is free of bugs and security holes, and that gets harder as agents write more of it. “Our Lean formalization is now the substrate that agents can build upon,” Swaminathan said.
I’d treat the jump from math to production software as a thesis, not a result. Math has clean rules and a clear definition of correct. Real software has messy requirements, and a verified proof only shows that code matches its spec, not that the spec was right.
What comes next
Founded in March 2025 by Hong, a 25-year-old Stanford math PhD dropout, Axiom raised a $200 million Series A led by Menlo Ventures this March. It now has a flagship result to point to, and a dare to go with it: “I openly challenge all the coding companies to work on formalization at this scale.”
If you run agents on code, the practical takeaway is simple. Keep an eye on verification tooling, and think about which parts of your stack would justify proof-level guarantees. The real test for Axiom will be whether mathematicians and developers actually build on this library. More details are available in the original TechCrunch AI report.