Axiom formalizes the Stacks Project for AI agents

The Stacks Project was started in 2005 by Johan de Jong, a Columbia mathematician, and has grown through contributions from mathematicians. It covers topics from college-level algebra to advanced work in algebra, geometry and number theory. Columbia mathematician Peter Woit has described it as having “nothing else really comparable,” likening it to the Bourbaki books, which rebuilt mathematics from its foundations in the 20th century.

Axiom’s agents translated the project into Lean, a programming language used to express proofs. A proof assistant checks the code line by line; if it passes, the proof is logically sound. The task was more than verifying individual theorems: definitions and results throughout Stacks depend on one another, and the team needed to preserve those links across the codebase.

“Things that are big and things that are delicate in life just don’t go together,” Axiom CEO Carina Hong told TechCrunch, describing the challenge of keeping the results consistent. Hong, 25, left a Stanford mathematics Ph.D. program and founded Axiom in March 2025. The startup raised a $200 million Series A in March, led by Menlo Ventures.

Axiom gave its agents a broad hierarchy but allowed them to identify tasks and work in parallel, said Ashvin Swaminathan, a member of the company’s technical staff. The company also trained its own models for mathematics. Hong said an in-house Lean expert initially helped teach the agents mathematical judgment, which they later developed further.

Swaminathan said algebraic geometry had been a major gap in formalized mathematics, leaving researchers with little Lean-based work to build on. He said the Stacks formalization changes that. Axiom argues that verified results can serve as reusable foundations for later proofs and, eventually, software built by AI agents. “The more formalized proofs you have, the more formalized proofs you can make,” UCLA mathematician and Fields Medal winner Terence Tao has said.

The company’s broader bet is that formal verification can help address the risk of AI-generated errors in software as agents write more code. “I openly challenge all the coding companies to work on formalization at this scale,” Hong said.