Axiom Puts Algebra Geo’s Big Ref Into Lean

A month after a wave of AI-written proofs hit mathematics, Axiom answered with some 16 million lines of math that a computer has checked step by step.

On November 4, Axiom released a Lean formalization of the entire Stacks Project, the open-source reference that holds up much of modern algebraic geometry. The original text runs to roughly 7,500 pages. The translation runs to some 16 million lines of code, and every completed proof in it has passed the kernel of the Lean proof assistant, the small trusted program that accepts or rejects each logical step. Axiom calls the result the largest integrated, reusable library of formalized mathematics ever built.

stir

The timing is hard to miss. On October 6, OpenAI published 722 mathematical manuscripts that it said were produced by an unreleased internal model, grouped into 372 families of results across mathematics, theoretical computer science and physics. A day later it withdrew three after a sign error broke one argument and two papers built on top of it, and revised fourteen more. The catalogue settled at 719. Lean proofs accompany many of the results but not all of them, and outside mathematicians have sp/ent the weeks since sorting through claims that touch problems as famous as the Unique Games Conjecture and the exponent of matrix multiplication.

That is the problem Axiom has organized itself around. When AI can produce arguments faster than any person can read them, the only check that scales is a machine one, and a machine check is only as useful as the library underneath it. A new proof in algebraic geometry can lean on a long chain of results in commutative algebra, schemes, sheaves and cohomology before its own argument begins. Until this week, much of that chain had no Lean counterpart.

flow

Columbia University mathematician Johan de Jong started the Stacks Project in 2005 and ran it the way engineers run a large open-source software project. Every definition, lemma and theorem carries a permanent tag, every proof points to the exact tags it depends on, and hundreds of contributors have extended it over two decades. Axiom kept that architecture intact: its side-by-side viewer pairs each page of the original with its Lean code and an interactive dependency graph.

The work itself was done by what Axiom describes as a hierarchical swarm of AI agents working in parallel across that graph, translating statements, searching Mathlib for abstractions that already exist, writing proofs and keeping definitions aligned between chapters. The coordination was the hard part. Two agents can each prove true things about the same object using subtly different definitions, and Lean will accept both files while leaving them nearly impossible to combine later.

The more revealing output may be the mistakes it found. Axiom says the process surfaced dozens of statements in the Stacks Project that needed local repair, 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, where a faulty supporting lemma left a gap under a deeper theorem, found other routes through the literature to prove the original result.

extent

The formalization sits deliberately apart from the original. On October 21, de Jong asked that AI-generated comments and pull requests stay out of the upstream Stacks repository for the time being, and Axiom says it keeps its Lean code, counterexamples and fixes in its own repository. The project site also splits the library into two tiers: StacksCore, code a person has checked against the Stacks text and brought up to Mathlib standards, and a second tier that Lean checks but that has not yet been through that human pass.

A kernel check also has limits. It confirms that a proof follows from its statement, not that the statement says what the original text meant. Axiom says it handled that second question with multi-agent audits, automated cross-checks against the source text and targeted human review of foundational definitions and landmark theorems.

bet

None of this is a change of direction. On a July 9 episode of First Commit, the podcast from venture firm Notable Capital, hosts Eliya Elon and Laura Hamilton sat down with Hong, who left a Stanford PhD in March 2025 to found the company. According to the episode notes, she argued that frontier labs were skipping formal math as too data-scarce to be worth the effort, that a model answering in Lean can be verified simply by running the program, and that math transfers to other fields the way code does, with chip design, software verification and cryptography among the early payoffs.

Investors bought the argument early. Menlo Ventures led Axiom’s $200 million Series A in March at a $1.6 billion post-money valuation. Since then the company has released Lean formalizations of the bounded gaps between primes and, on October 27, the Classification of Finite Simple Groups, a theorem whose original proof took more than a hundred mathematicians decades. Hong told TechCrunch she wants rivals to follow: “I openly challenge all the coding companies to work on formalization at this scale.” The Stacks library, meanwhile, takes outside contributions through open claims on its project site, each requiring a written blueprint before any Lean is submitted.