Axiom Math: Stacks Project formalized in Lean by AI agents

Felix Laurent 5 Nov 2026 4 min read

AI agents

Axiom Math has formalized the Stacks Project, one of the largest reference works in modern mathematics, in the Lean proof assistant. The startup announced the release on November 4, 2026. AI agents translated the roughly 7,500-page library into about 16 million lines of Lean code, and Lean's kernel checks every proof in it.

The timing matters. AI systems now produce mathematical proofs faster than people can read them, and Axiom is betting that the answer is to check them by machine. "Most think vibecoding at scale is slop. Here's a counterexample," the company wrote on X.

What the Stacks Project is

Columbia mathematician Johan de Jong started the Stacks Project in 2005 as an open reference for algebraic geometry. It grew over two decades into a single connected text that runs from basic commutative algebra to advanced work on schemes and algebraic stacks. Every result has a permanent four-character tag, so other papers can cite it precisely.

That structure makes it hard to formalize. Thousands of results depend on one another, and a formal version has to keep every one of those links intact. Ashvin Swaminathan of Axiom's technical staff told TechCrunch that formalized mathematics has "this huge black hole" in this area. Axiom's library is meant to fill it.

How Axiom's AI agents did it

Axiom used what it calls coordinated swarms of AI agents, run on models the company trained for math. The team gave the agents a loose structure and let them work in parallel. According to Swaminathan, the agents were soon "finding tasks for themselves." Early on, an in-house Lean expert taught them what good formal code looks like.

The result is one Lean 4 library built on Mathlib, Lean's main math library. Each Stacks tag maps to a Lean declaration, and the project site shows the original pages next to the code. According to the repository, the proofs contain no sorry placeholders and rely only on Lean's three standard axioms. Examples, exercises and remarks are not formalized yet.

The library has two parts:

StacksCore holds code that human maintainers have reviewed against the original;
StacksFrontier holds AI-written code that has not been reviewed yet.

The code is open on GitHub under the Apache 2.0 license.

The agents found errors in the original

The process also tested the Stacks Project itself. Axiom says its system surfaced dozens of statements that needed local fixes. Some lacked hypotheses, some broke in positive characteristic, and some did not hold in the generality stated. For some of them the agents built explicit counterexamples and formalized the corrected theorem next to them. Where a false supporting lemma left a gap, they found another route through the literature.

The same thing happened a week earlier. On October 26, Axiom released a formal proof of the Classification of Finite Simple Groups, which it calls the first complete computer-checked version. That project took 24 days and about 43.1 million lines of Lean. Axiom reported 34 notable deviations from the published record, including a gap in a 1986 proof that its agents had to repair.

Errors like these explain why the release drew attention well beyond Lean users. They also raise the question of who checks the checker.

What Lean checks and what it does not

Lean verifies that each proof follows from its statement. It cannot tell whether the statement says what the original text meant. Axiom says it checked that through multi-agent audits, cross-checks against the source and targeted human review of key definitions and theorems. The company has not said how much of the library people have read line by line, and StacksFrontier is unreviewed by design.

The mathematicians behind the original are cautious too. On October 21, de Jong asked people not to send AI-written comments or pull requests to the Stacks Project. He wrote that he intends to keep updating it by hand for the near future. Axiom's library therefore stays separate from the upstream project. Axiom says it wants to move as much as it reasonably can into Mathlib, which means more human review first.

That caution is part of a wider debate. Last month OpenAI released 719 manuscripts claiming solutions to hard open problems, and TechCrunch reported that mathematicians found they did not meet the field's standards. In October, OpenAI, Anthropic and the Simons Foundation committed $15 million to help mathematicians verify AI proofs. Machine-checked results, like the Lean proof behind the KLS conjecture, are becoming the bar.

Who is behind Axiom Math

Carina Hong, 25, founded Axiom in 2025 after leaving a Stanford math PhD. In March 2026 the company raised a $200 million Series A led by Menlo Ventures at a $1.6 billion post-money valuation. Menlo said at the time that Axiom's prover had scored 12 out of 12 on the December 2025 Putnam exam.

Axiom pitches formal verification beyond pure math, as a way to prove that AI-written software works. Swaminathan calls the Stacks library "the substrate that agents can build upon." Hong went further: "I openly challenge all the coding companies to work on formalization at this scale."

Does Axiom's Stacks Project formalization keep AI slop out of math

Partly, and in the way that counts most. Anyone can check a Lean library with no sorry by running a build. No pile of AI-written manuscripts offers that. The errors the agents found in the Stacks Project and in the finite simple groups proof show that formalization also improves the human record.

The open question is the statements. Until mathematicians review StacksFrontier and the work moves toward Mathlib, the library is verified proof attached to partly unverified translation. Axiom has shown that AI agents can produce formal mathematics at the scale of a whole field. Whether the field adopts it now depends on human reviewers, and de Jong has made clear they will set the pace.