SeaPRwire – Axiom Math said on Wednesday that it had formally verified the Stacks Project, a reference work of roughly 7,654 pages spanning algebra, geometry and number theory, and turned it into about 16 million lines of code that a proof assistant checks line by line.
Formal verification means rewriting a proof in Lean and having a program test every step. If the code compiles and the checker accepts it, the proof is sound in the narrow sense that it follows from its axioms. Whether it is the theorem a reader of page 4,000 had in mind is a separate question, and one the announcement does not address.
The concern behind the work is not hypothetical. Last month OpenAI published 719 manuscripts claiming results on hard problems, and the automated checks used to confirm that kind of output can fail, according to an arXiv paper on the subject.
Stacks is an unusual thing to verify. Johan de Jong, a Columbia mathematician, started it in 2005 as an open source reference, and contributions have accumulated since, from first-year algebra to results at the edge of current research. Peter Woit, also at Columbia, has compared it to the Bourbaki volumes that rebuilt the field’s foundations in the twentieth century.
The work was done by a fleet of Axiom’s agents running in parallel. Ashvin Swaminathan, who works on the technical staff, said the team imposed a hierarchy without dictating what each agent did: “The agents were finding tasks for themselves and identified things that they could work on in parallel.”
Keeping 16 million lines consistent is harder than writing them. Every theorem in Stacks rests on earlier theorems and definitions, so a translation that gets one dependency wrong can produce a structure that compiles and still does not match the source. Carina Hong, the chief executive, described the difficulty in terms of scale and fragility rather than error: “Things that are big and things that are delicate in life just don’t go together.”
The ratio is worth a look. Sixteen million lines against 7,654 pages works out to roughly 2,000 lines of Lean for every page of prose. A formal proof spells out steps a human reader supplies silently, so a large multiple is expected. It also means the surface a reviewer has to check is two thousand times the text it mirrors.
Axiom trained its own models for the job and started by having an in-house Lean expert teach the agents judgment about which formalization was worth writing. Hong said the agents have since developed that judgment on their own. That claim is the part of the project an outside reader cannot check from the announcement.
Hong framed the alternative approach as licensing models and building tooling on top of libraries that already exist, which she said is what most verification startups do. Training in house, on her account, is what let the agents work at this scale. A customer cannot test that claim before buying.
The gap the work fills is specific. Swaminathan called algebraic geometry “this huge black hole” in formalized mathematics, which meant researchers who wanted to machine-check a new result in the field had little to build on. Those researchers now have a library to import.
Using it is a different skill from building it. Anyone who imports Stacks inherits every definition it carries, including the conventions Axiom’s agents settled on where the source text left one open. Those choices sit at the top of a formalization and are the first thing a specialist reads.
None of that shows up in a page count.
Axiom’s argument for why that matters is cumulative. Each verified result becomes something a later proof can cite instead of rederiving, and Terence Tao, the UCLA mathematician, has put the effect plainly: “The more formalized proofs you have, the more formalized proofs you can make.”
The company is valued at $1.6 billion and raised a $200 million Series A in March led by Menlo Ventures. Hong, 25, left a Stanford mathematics PhD to start it in March 2025.
Its commercial case rests on the same mechanism applied to software. Developers have never been able to guarantee that code is free of defects, and the problem grows as agents write more of it. A verified library is a way to check an agent’s output against something other than another model’s opinion.
For a coding agent, that changes what a check is. The usual test of generated code today is another model reading it, or a suite of tests a person wrote in advance. Formal verification offers a third option: the agent’s output is turned into a formal statement and tested against definitions that were themselves tested.
Stacks is not the only possible target, only the largest one so far.
The Stacks work says something about the method as well as the result. Axiom’s agents chose their own tasks inside a loose hierarchy, which is closer to how the company expects agent labour to be organised than a pipeline of assigned steps. Hong’s reason for caring is that early structural mistakes are expensive to undo: “If you slop drop in a way that’s bad engineering choices in the beginning, then it’s very hard for them to grow that boundary.”
What the announcement does not include is independent confirmation. Formal verification is checkable by anyone with the code and a proof assistant, which is the point of it, and that check has not yet been published by a third party. Nor has Axiom said how many mathematicians reviewed the translation against the source text rather than against the compiler.
The company has been direct about wanting the field to follow. Hong’s closing line was a challenge to the coding companies to formalize at the same scale, which is a claim about where the bottleneck sits: not in the checking, but in the willingness to pay for it.
Until someone outside Axiom imports the library and builds a new proof on top of it, the Stacks formalization is a demonstration that the translation can be done. It is not yet evidence about what the translation is good for.