Axiom says it has formalised the whole Stacks Project in Lean

Axiom said on 4 November 2026 that it is releasing a Lean formalisation of "the entire Stacks Project", the online algebraic geometry reference started by Columbia University mathematician Johan de Jong, and describes the result as "the largest integrated, reusable library of formalized mathematics ever built". The code is public on GitHub under the Apache 2.0 licence.

What Axiom says it has built

In its announcement, Axiom describes the Stacks Project as "the roughly 7,500-page open-source reference that lays the foundations of modern algebraic geometry" and says the formalisation spans "some 16 million lines of code". The Stacks Project's own site currently lists 7,654 pages, 21,446 tags and 116 chapters.

The data file behind Axiom's companion site, stacks.axiommath.ai, generated on 4 November, puts the library at 15,751,904 lines of Lean across 62,975 files and 663,090 declarations. The repository's README gives "about 63,000 modules" and warns that "a full build takes a long time and a lot of memory".

Axiom says the work was done by "coordinated swarms of AI agents capable of translating, proving, and integrating thousands of theorems in parallel", organised as "a hierarchical system of AI agents with specialized responsibilities and strict coordination protocols". It also says its system "surfaced dozens of statements in the Stacks Project that required local refinement, including missing hypotheses, edge cases in positive characteristic, and claims that did not hold in the full generality stated".

The announcement does not name a model. The repository's metadata file lists one, AxiomProver, which it describes as Axiom's "in-house theorem proving system", and says the formalisation "was generated collaboratively between human formalisers at Axiom Math and AxiomProver".

What "entire" covers

The repository is more specific than the headline. Its README says: "We have formalized every tag of the Stacks Project with formalizable content". It adds that "Examples, exercises and remarks that are not yet formalized are left as tasks for contributors", and the metadata file says "The exercises and obsolete chapters are out of scope", with statements taken from a fixed snapshot of the Stacks Project covering "Chapters 1 to 109".

The library is split into two tiers:

• StacksCore: "human-reviewed formalizations, checked against the Stacks Project and brought to Mathlib standards".
• StacksFrontier: "formalizations written by AI agents", which the metadata file says "builds with no sorry and only the standard axioms, and each statement was checked against its Stacks tag, but it has not yet had human review". It also says "most of StacksFrontier formalised autonomously", and gives the review status as "self-assessed".

On proof gaps, the README states: "There is no sorry and no native_decide", and that proofs "use only the standard axioms propext, Classical.choice and Quot.sound". The metadata file records a sorry_count of 0. We did not build the library or run our own count of sorry in the code; those figures are Axiom's.

The site's data file also lists 16,249 "formalizable" tags and 16,219 completed, of which 1,377 are counted as already in Mathlib. The remaining 30 are grouped under labels reading CONDITIONAL (9), PARTIAL (15) and WRONG (6); the file does not explain the labels, though the companion site's interface displays the WRONG status as "needs correction".

The "largest" claim

The "largest" label is Axiom's claim, and the post does not say what it is measured against. For one point of comparison: the statistics page for Mathlib, the community Lean library this project builds on, lists 139,864 definitions and 293,257 theorems, and its underlying data file, generated on 8 November, gives Mathlib 2,499,686 lines across 9,477 files. On our reading, line counts are not a like-for-like measure of how much mathematics a library holds, and the Stacks library depends on Mathlib rather than replacing it.

Reaction

On 21 October, two weeks before the release, de Jong posted "No AI for now" on the Stacks Project blog, asking: "Please for now do not have your AI leave comments or leave comments containing material written by AI or have your AI do pull requests or submit pull requests containing material written by AI." Axiom's post cites that request and says "We fully respect that boundary: we keep our formalization, counterexamples, and refinements in our own repository".

Under de Jong's post, a commenter, Maarten Derickx, wrote, in reply to a question about forks, that "the stacks project license does permit creating derivative works", while adding that doing so without talking to de Jong first "will be a sign of poor social judgement". The README notes that the Stacks Project itself is licensed under the GNU Free Documentation License.

On Hacker News, where the post had drawn 26 comments when we checked on 8 November, reaction was mixed. One commenter wrote: "Okay this is actually useful AI formalization." Another said they "would be interested in hearing more about the gaps they uncovered in the existing results". Several criticised the announcement's prose, one calling it "AI slop", and a separate commenter asked: "Why would mathematicians want to build upon a corporate product?"

Why it matters

Axiom says the library lets "Researchers and AI agents alike" import its definitions and theorems "directly into new formal proofs". On our reading, the open questions are how much of the AI-written StacksFrontier tier survives human review, and how the project sits alongside a Stacks Project whose maintainer has asked for AI contributions to stay out for now.