AxiomMath announced it has completed a formal verification of the Stacks Project, converting the reference’s roughly 7,654 pages into about 16 million lines of Lean code that a proof assistant can check.
What the project entailed
The Stacks Project, started by Johan de Jong in 2005, is an extensive open-source library of results spanning algebra, geometry and number theory. Mathematicians often regard it highly; Columbia mathematician Peter Woit compared it to the Bourbaki books.
AxiomMath said its fleet of AI agents translated the human-written material into code that a proof assistant checks line by line. Formal verification reproduces proofs in a programming language (in this case, Lean) so a checker can confirm the arguments are logically sound. The company noted that formal verification is also used in engineering — for example, to validate chip designs and to find bugs in government software.
How AxiomMath worked
The company said agents worked in parallel under a loose hierarchy so they could discover and take tasks independently while preserving interconnections across the library. AxiomMath staff member Ashvin Swaminathan described the work as preserving every dependency and keeping the Stacks Project’s structure intact across millions of lines of code.
AxiomMath reported that it trained its own models to perform well on mathematical formalization and initially relied on an in-house Lean expert to teach the agents a human sense of correctness. Over time, the agents reportedly developed that judgment autonomously, the company said.
The startup emphasized that formalized results become building blocks: checked theorems can be reused rather than rederived from scratch. Terence Tao, UCLA mathematician and Fields Medal winner, was quoted as saying that “the more formalized proofs you have, the more formalized proofs you can make.” Swaminathan added that the work fills a large gap in formalized algebraic geometry, giving researchers a foundation to build on.
AxiomMath described itself as a $1.6B startup. The company said its 25-year-old CEO, Carina Hong, who left a Stanford math Ph.D. program, founded the firm in March 2025; in March the company raised a $200 million Series A led by Menlo Ventures. Hong told reporters she wants a reusable, verified body of knowledge to prevent what she called “slop” in AI outputs and publicly challenged other coding companies to pursue formalization at comparable scale.
Original source: TechCrunch AI