Axiom Math verifies the Stacks Project to curb AI slop in math

How the verification works

Mathematicians rewrite a proof as code in a programming language called Lean, and a proof assistant checks it line by line. Engineers use the same idea, called formal verification, to confirm chip designs, and researchers in France have used it to catch bugs in software that calculates family benefits.

Stacks was a hard test because its theorems and definitions depend on one another, much like a family tree. Columbia mathematician Johan de Jong started the open source project in 2005, and it now spans material from college-level algebra to advanced algebraic geometry and number theory. "Things that are big and things that are delicate in life just don't go together," CEO Carina Hong said.

Axiom gave its agents a loose hierarchy and let them run in parallel, picking their own tasks. The company also trained its own math models. Technical staff member Ashvin Swaminathan said formalized math had a "huge black hole" in algebraic geometry, which researchers using Lean can now build on.

Beyond mathematics

Axiom argues each verified result becomes a building block, echoing Terence Tao's remark that "the more formalized proofs you have, the more formalized proofs you can make." The target audience also includes developers, who struggle to guarantee code is free of bugs and security holes, a problem that grows as AI agents write more software.

Hong, 25, dropped out of a Stanford math PhD program and founded Axiom in March 2025. The company raised a $200 million Series A led by Menlo Ventures in March. She expects agents to need reusable, verified libraries to avoid producing slop, and openly challenged all coding companies to "work on formalization at this scale."