AI systems are making increasingly bold claims about solving difficult math problems, but even computer checks can fail. Axiom Math is betting that formal verification can help keep mathematical work reliable: its agents have translated the Stacks Project into code that a proof assistant checks line by line.
A large reference, rebuilt as checked code
The Stacks Project began in 2005 as an open-source reference. Started by Johan de Jong, it has grown through contributions from mathematicians and covers subjects from college-level algebra to advanced ideas in algebra, geometry and number theory. Columbia mathematician Peter Woit has described it as having “nothing else really comparable,” likening it to “the famous Bourbaki books.”
Axiom says its agents translated the roughly 7,654-page library into about 16 million lines of Lean code. Lean is a programming language used to express proofs. A proof assistant checks that code line by line; when the proof passes, the result has been checked for logical soundness.
That process, known as formal verification, is also used in engineering to check chip designs and in software research to catch bugs. The aim is not simply to put individual theorems into a computer. The surrounding definitions and results must continue to fit together.
Keeping the mathematical connections intact
Results in the Stacks Project depend on earlier results, much like branches in a family tree. Axiom initially questioned whether it could preserve those links throughout such a large conversion. The challenge was to make sure the definitions did not conflict and theorems remained consistent across the library.
CEO Carina Hong told TechCrunch that the team was unsure whether “vibe coding” could preserve the project’s “beauty.” Axiom gave its agents an overall hierarchy but did not prescribe every task. According to Ashvin Swaminathan, a member of the technical staff, agents identified work they could do in parallel and found tasks for themselves.
The company also trained its own models for mathematics. Hong said the team initially relied on an in-house Lean expert to teach agents a human sense of taste; she said the agents have gradually developed that taste themselves.
A resource for an underrepresented field
Axiom says the completed formalization addresses a major gap in computer-checked mathematics: algebraic geometry. Swaminathan said researchers previously had little Lean material to build on when they wanted to check new work in the field. The Stacks Project gives them a larger base of formalized results and definitions to use.
The practical value of a verified library is cumulative. If a result has already been checked and its dependencies are available, later proofs may be able to build on that work instead of recreating it. UCLA mathematician and Fields Medal winner Terence Tao has expressed the general idea this way: “The more formalized proofs you have, the more formalized proofs you can make.”
Each addition can make the library more useful to the next researcher or agent. That promise depends on keeping the shared foundation dependable: errors or poor choices embedded early can complicate work built on top of them.
From mathematical proofs to software
Axiom’s ambitions extend beyond mathematics. Developers have long struggled to guarantee that software has no bugs or security holes, and the challenge grows as AI agents write more code. The company argues that formal verification skills developed through mathematical proofs can transfer to software infrastructure.
Swaminathan described Axiom’s Lean formalization as a substrate agents can read, understand and extend. In that vision, agents use a reusable body of checked knowledge to build new systems, rather than relying on unverified output alone.
Founded by Hong in March 2025, Axiom raised a $200 million Series A led by Menlo Ventures in March. The company’s large-scale Stacks effort is also a challenge to other coding companies: Hong said she openly challenges them to work on formalization at this scale.