AI systems are cracking math problems at a rate that makes verification hard to trust: OpenAI alone released 719 manuscripts last month claiming solutions to some of the field’s hardest problems, and even computer checks can slip. Axiom Math, a $1.6B startup founded in March 2025 by 25-year-old Carina Hong, is betting mathematics can avoid AI slop by standing on firmer ground instead of slowing down. The company has raised a $200 million Series A led by Menlo Ventures. On Wednesday, it announced that it has formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. Columbia mathematician Peter Woit has compared the project to the famous Bourbaki books, saying there is ‘nothing else really comparable.’ The project began in 2005 when Columbia mathematician Johan de Jong created it as an open-source reference; mathematicians have since expanded it from college-level algebra into advanced algebra, geometry, and number theory. Axiom’s fleet of AI agents translated the library’s roughly 7,654 pages into about 16 million lines of computer-checked Lean code.

Formal verification means rewriting proofs as code in the Lean programming language and having a proof assistant check the code line by line; if the proof passes, it is logically sound. Engineers already use the same idea to check chip designs, and researchers in France have used it to catch bugs in software that calculates family benefits. But the Stacks Project is especially delicate because its results are interconnected, each building on the ones before it. Axiom was unsure the project would work: the team had to preserve every connection across roughly 16 million lines. “Things that are big and things that are delicate in life just don’t go together,” Hong told TechCrunch.

To get there, Axiom gave its agents a loose hierarchy and let them choose tasks and work in parallel rather than dictating every move. The team also trained its own models to be good at math, an approach Hong says most verification startups have not taken; an in-house Lean expert initially taught the agents a sense of taste, which Hong says the agents later developed on their own. Hong acknowledged the team was not sure vibe coding would preserve the beauty of Stacks.

The result fills what Axiom describes as a huge black hole in formalized math covering algebraic geometry. Ashvin Swaminathan, a member of the technical staff, said researchers who want to check new work in algebraic geometry with Lean previously had little to build on; now they do. Each verified theorem is meant to become a building block that future proofs can rely on instead of starting from scratch, which is how formalization compounds. Terence Tao put it simply: “The more formalized proofs you have, the more formalized proofs you can make.”

Mathematicians are not the only intended audience. Developers have long struggled to guarantee code is free of bugs and security holes, and that problem grows as AI agents write more code. Axiom believes mathematics is the domain where verified foundations should start, and that the skills transfer: agents can read its Lean code, understand it, and build new infrastructure on top of it. Hong sees the parallel, self-directed workflow behind Stacks as a model for future AI work, arguing agents need a reusable, well-built library to keep pushing the frontier; bad engineering choices early on make it hard for the boundary to grow. She closed with a challenge: “I openly challenge all the coding companies to work on formalization at this scale.”