Axiom’s Stacks Formalization: 16M Lines of Lean, Explained

A mathematical city in Lean

Most think vibecoding at scale is slop. Here’s a counterexample.

Axiom describes the result as a 16-million-line formalization of the entire Stacks Project, which it calls critical infrastructure underlying modern math. The company presents the code as optimized and as keeping the project’s highly interconnected structure intact, and it frames the whole artifact as a mathematical city.

Editor notes on the announcement add that AI agents carried out the formalization and that Axiom is releasing the Lean code as open source. The Stacks Project itself is the long-running open encyclopedia of algebraic geometry, running past 7,500 pages.

Why this corpus is a severe test

The Stacks Project is a single, densely cross-linked body of algebraic geometry. Formalizing all of it means every definition, lemma, and reference has to live in Lean, a proof assistant whose files only check if the logic actually holds together.

Axiom’s pitch is aimed at the suspicion that large-scale AI coding produces unmaintainable output. Preserving the encyclopedia’s web of dependencies, rather than flattening it into isolated snippets, is the property the announcement treats as the point.

• Scale

  Sixteen million lines, covering the whole project rather than a chapter or a toy theorem.

• Structure

  The highly interconnected layout of the Stacks Project is described as preserved.

• Code quality

  Axiom says the generated Lean was optimized, and offers that as the counterexample to sloppy vibecoding.

What is public, and what is still unknown

You cannot clone, browse, or build this formalization from an official page today. Axiom has only shown it in a short preview video and the November 4, 2026 announcement, even though that announcement speaks of a release and the accompanying notes call the Lean open source.

Nothing published so far specifies a repository, a license text, a build recipe, hardware requirements, or how much of the 16 million lines has been machine-checked end to end. There is also no app, API, model card, weight release, or price, because this is a code formalization rather than a hosted model you can call.

Where a corpus like this would matter

If the files do check in Lean, a complete formal Stacks Project would give algebraic geometers a machine-readable map of the same encyclopedia they already cite, with definitions and lemmas wired together instead of living only as prose.

Until a public tree exists, realistic use stops at the claim itself: a data point about AI agents writing formal mathematics at encyclopedia scale. Comparison with other proof efforts, proof-coverage percentages, and error rates are not in the announcement, so those questions stay open.