Axiom Math wants to keep AI slop out of mathematics

Axiom Math, a startup valued at $1.6 billion, announced Wednesday that its fleet of AI agents has formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. The announcement arrives amid a surge of AI-generated mathematical claims: OpenAI alone released 719 manuscripts last month asserting solutions to some of the field's hardest problems, and even computer checks can slip.

The Stacks Project began in 2005 as an open-source reference started by Columbia mathematician Johan de Jong, with contributions ever since spanning college-level algebra up through advanced work in algebra, geometry, and number theory. Columbia's Peter Woit has said there is "nothing else really comparable," likening Stacks to "the famous Bourbaki books." Axiom's agents translated the library's roughly 7,654 pages into about 16 million lines of computer-checked code written in Lean, a proof assistant that checks each line for logical soundness.

The scale was the hard part. Theorems and definitions in Stacks are interdependent, each building on prior results, so the team had to keep every connection intact across the full codebase — an interlinked structure the company said made it uncertain the project would succeed at all. CEO Carina Hong, 25, who dropped out of a Stanford math Ph.D. program to found Axiom in March 2025, described the tension between size and precision: "Things that are big and things that are delicate in life just don't go together." She added that the team "were not sure if vibe coding would be able to preserve the beauty of Stacks."

Formal verification is an established technique beyond mathematics — engineers use it to confirm chip designs, and researchers in France have applied it to software calculating family benefits. Axiom's framing extends that idea into a product bet: a verified foundation that AI agents can rely on when writing software and, eventually, doing science.

What to watch is whether the verified library becomes infrastructure others build on, and whether verification scales beyond a single landmark project. Open questions include how Axiom maintains Stacks as human mathematicians keep contributing, whether its agents can verify comparably tangled libraries, and how much of the broader flood of AI math claims the approach can actually absorb.