OpenAI alone put out 719 manuscripts last month claiming progress on hard math problems. Even computer checks can slip. If you’ve watched what AI did to search results and stock images, it’s fair to ask whether math is next.
Axiom Math is betting it doesn’t have to be. The company announced that it formally verified the Stacks Project, one of the largest bodies of human-written mathematics. Johan de Jong started Stacks in 2005 as an open-source reference, and it now runs about 7,654 pages from college algebra to advanced algebraic geometry and number theory. Columbia’s Peter Woit says there’s “nothing else really comparable.” Axiom’s agents translated it into roughly 16 million lines of Lean, checked line by line by a proof assistant.
Formal verification isn’t new. Chip makers use it, and French researchers have used it to catch bugs in software that calculates family benefits. The hard part here was scale and consistency. Stacks results build on one another like a family tree, so one broken link can spoil what sits above it. CEO Carina Hong admitted the team wasn’t sure the project would work.
The method is the interesting bit. Axiom gave its agents a loose hierarchy and let them pick tasks and run in parallel. It also trained its own math models, which Hong says most verification startups haven’t done. Compare that with DeepMind’s AlphaProof, which targets competition-style problems, or Harmonic’s Aristotle, which also works in Lean. Axiom is going after infrastructure instead of headline proofs.
That matters because algebraic geometry has been a “huge black hole” in formalized math, in the words of Axiom engineer Ashvin Swaminathan. Researchers checking new work in the field had little to build on. Now they do. Terence Tao’s point applies: the more formalized proofs exist, the more you can make.
But the bigger pitch is for developers. As agents write more code, nobody can review it all by hand. Axiom argues that verified libraries give agents something solid to build on, so they don’t pile mistakes on top of mistakes. Hong’s line is blunt: bad engineering choices early on make it hard for agents to push the frontier later.
Is it noise? Not the Stacks result. It’s concrete, checkable, and useful to mathematicians today. The claim that this becomes a foundation for trustworthy AI-written software is still a bet. Verification is slow and expensive, and most teams ship without it. Still, with a $200 million Series A led by Menlo Ventures and a 25-year-old CEO daring coding companies to match this scale, Axiom is worth watching. If agent-written code keeps growing, someone has to make it provable.
