Axiom Math turns a 7,500-page algebraic geometry reference into code a computer can check

Axiom Math, a startup founded in March 2025, released a Lean formalization of the entire Stacks Project on November 4, a library of about 16 million lines of machine-checked code, the company said. It built the library with coordinated groups of AI agents.

A reference text turned into code a computer can check

The Stacks Project is an open-source reference of roughly 7,500 pages on the foundations of modern algebraic geometry, which Columbia University mathematician Johan de Jong started in 2005, according to Axiom. Lean is a programming language in which a proof is written as code that a proof assistant checks line by line, TechCrunch explained.

Axiom said the library is the largest integrated, reusable library of formalized mathematics ever built. That is the company's own description. It said researchers and AI agents can import its definitions and theorems into new formal proofs, and that permanent Stacks tags link each Lean declaration to the original text.

How the work was organized

Axiom said it designed a hierarchical system of AI agents with specialized responsibilities and strict coordination protocols, working in parallel across the project's dependency graph. Ashvin Swaminathan, a member of Axiom's technical staff, told TechCrunch that the team imposed a hierarchy but "it was not, like, a complete hierarchy of dictating what every single agent was doing."

Axiom CEO Carina Hong told TechCrunch the company also trained its own models to be good at math, an approach she said most other verification startups have not taken.

What the formal check found in the text

Axiom said the process surfaced dozens of statements in the Stacks Project that needed local refinement, including missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated. Its agents built explicit counterexamples and repaired the downstream proofs, the company said. These findings come from Axiom's post, and the post does not say that the Stacks Project's maintainers have reviewed them.

The company noted that de Jong asked in an October 21, 2026 announcement that AI-generated comments and pull requests not be submitted to the upstream Stacks Project repository for the time being. Axiom said it respects that request and keeps its formalization, counterexamples and refinements in its own repository.

Who is behind it, and what it has raised

Hong, who is 25, dropped out of a Stanford mathematics PhD program to found the company, TechCrunch reported. Axiom raised a $200 million Series A in March led by Menlo Ventures, TechCrunch said, and described the company as a $1.6 billion startup. The valuation is TechCrunch's figure and Axiom's post does not state one.

The Stacks release followed Axiom's October 27 release of a formalization of the Classification of Finite Simple Groups, the company said. Axiom has not published revenue or customers, and its post names no paying users of the library.

A milestone that is free to use, so the business is still unproven

We think the Stacks release shows what Axiom can build more clearly than it shows what it can sell. Verified foundations are a plausible need as AI agents write more code, as Hong argues, but the library is open source and the sources name no customer. Funding is a milestone, not proof.

The opportunity is that checked mathematics becomes a base other work can reuse. The threat is that the company has to turn a public good into revenue. We expect the next test to be a named paying use outside mathematics, and we would change our view if the library is adopted widely by researchers while the company still discloses no commercial uses.

The view in this final section is FinanceInTime's editorial opinion, for information only. It is not investment, tax, legal or other advice, and it does not take your circumstances into account. Forecasts are uncertain and past results do not guarantee future ones.