Axiom has released an open Lean 4 formalization of the Stacks Project, which it says runs to about 16 million lines. The announcement came from Axiom's official X account on November 4, 2026. It describes a "16M-line formalization of the entire Stacks Project," with "optimized code quality and its highly interconnected structure preserved."
The code is public in the AxiomMath/Stacks repository under Apache 2.0. This post explains what is in it, what the two-tier layout means, and what is still unverified.
TL;DR: the facts in one table
| Question | Answer |
|---|---|
| What is it? | A Lean 4 formalization of the Stacks Project, the open-source reference on algebraic geometry |
| Size? | About 16M lines, per Axiom's X post; we did not count lines |
| Who wrote it? | A mix: human-reviewed code in StacksCore, AI-agent code in StacksFrontier |
| License? | Apache 2.0 (the Stacks Project itself uses the GNU Free Documentation License) |
| Built on? | Mathlib, Lean 4 version 4.34.0-rc2 |
| Proof quality? | README: Lean's kernel checks every proof; no sorry, no native_decide |
| Complete? | Every tag with formalizable content; examples, exercises and remarks partly open |
| Can I help? | Yes, review and contribution are welcome |
What is the Stacks Project, and why formalize it?
The Stacks Project is a large, open, online reference work on algebraic geometry. Researchers cite it by short alphanumeric tags, which makes individual statements easy to point to. It is a standard dependency for current work in the field, and it is the kind of text where one wrong lemma can quietly affect many later papers.
The Lean side rests on Mathlib, the community library of formalized mathematics. Mathlib already covers a large part of commutative algebra and some algebraic geometry, which is why the README can register some Stacks tags directly on existing Mathlib declarations. Axiom's contribution is the large remainder, plus the tag layer that ties each declaration to the source text. For a working mathematician, that tag layer may be as valuable as the proofs: it makes the library searchable in the same vocabulary the field already uses.
A Lean formalization turns those statements and proofs into code that a small trusted kernel can check. The payoff is trust and reuse. If a later theorem depends on a Stacks result, a machine can confirm the chain. For AI systems, a large verified library is also a training and grounding resource: an agent proving a new statement can build on existing, checked lemmas.
Axiom's earlier work shows the direction. In October the company said its system formalized the Classification of Finite Simple Groups; we covered that in our claimed-versus-verified post on the CFSG formalization. The Stacks release is a different kind of artifact: instead of one famous theorem, it is infrastructure that many results depend on.
How is the repository organized?
The README describes a structure with two tiers, both pulled in by import Stacks.
- StacksCore holds human-reviewed formalizations. They are checked against the Stacks Project and brought to Mathlib standards for naming, generality and style.
- StacksFrontier holds formalizations written by AI agents. The README calls it the place "where coverage grows fastest, and where review is most needed before code moves into StacksCore."
This split is the most useful honest detail in the release. It tells you that a large share of the code was produced by agents and has not yet had the human review that Mathlib normally expects. Every proof in either tier is kernel-checked, so the statements are proven. What review adds is confidence that the statements say what the Stacks Project says, and that the code is readable and maintainable.
How do you find a result?
Declarations that formalize a Stacks tag carry an attribute such as @[stacks 00DS]. Where Mathlib already covers a tag, it is registered on the Mathlib declaration instead. After importing the library, the command #stacks_tags lists every tagged declaration, and #stacks_tags! also prints each statement. A website links each tag to its Lean code, its dependencies and the original Stacks statement.
The repository also tags declarations with items from Grothendieck's EGA and SGA. A tag is applied only when the declaration proves the whole item, a more general statement, some of its clauses, or a special case, and the comment says which.
Why the "kernel-checked" claim matters, and what it does not cover
The README states: "Lean's kernel checks every proof. There is no sorry and no native_decide." That is a strong, checkable property. A sorry is a placeholder for an unfinished proof. native_decide runs compiled code to settle a statement, which moves trust outside the kernel. Excluding both means the proofs stand on Lean's core and Mathlib.
Kernel checking does not tell you three things:
- Fidelity of statements. A proof can be correct for a statement that is subtly different from the paper statement. Review against the source is how that is caught. That is the job of the StacksCore tier.
- Quality of code. Machine-written proofs can be long and hard to read. Mathlib maintainers care about generality and style because the library has to be maintained for years.
- Coverage claims. The README says every tag with formalizable content is done. We did not audit tags, and the repository shows a single commit, so history of how it was built is not visible.
What about the 16 million lines?
The figure comes from Axiom's X post, and the repository README does not state a line count in the text we read. We did not clone and count. Line counts are also a weak measure: generated Lean can be verbose, and a bigger number is not automatically better. A fairer measure is how many Stacks tags are covered and how much of the code passes human review over time.
Axiom's framing is also a claim about method: that AI-written code at scale does not have to be sloppy. The two-tier design reads as an admission that review is still the bottleneck, which is consistent with the broader pattern in AI-for-math. Systems can produce a lot of checked code quickly, and people then decide what is worth keeping. Our posts on Lean 4 and the collapse in formal proof cost and on OpenAI's Lean reinforcement learning environments cover the same trend from other angles.
How does this compare with other recent AI-and-Lean claims?
| Item | Type | Evidence |
|---|---|---|
| Axiom Stacks Project | Open repo, Apache 2.0 | Public code, kernel-checked, two review tiers |
| Axiom CFSG | Open repo, large formalization | Self-reported scale; see our claimed-vs-verified post |
| Fermat's Last Theorem effort | Research claim | See our post on Claude and Fermat's Last Theorem in Lean |
| Quantum problem proofs | Company claim | See our claimed-vs-verified post |
The Stacks release stands out because anyone can inspect, build and review it. That is the difference between a press claim and an artifact.
How to try it
- Install Lean 4 and Lake. The repository pins its toolchain in the
lean-toolchainfile, so use the version it names. - Clone the repository. Use the GitHub link above and read the README and CONTRIBUTING.md first.
- Fetch dependencies. The
lake-manifest.jsonlists Mathlib and other packages. Expect a large download and a long first build. - Import and explore. Use
import Stacks, then run#stacks_tagsto list tagged declarations. - Spot-check a tag. Pick a result you know, open its tag on the Stacks Project site, and compare the Lean statement to the text. This is the review step the project asks for.
Mind your hardware. A 16-million-line library is heavy to compile. If you only need a slice, import the core tier or a single module.
What this means for builders and learners
For readers who build with AI, the lesson is about verification. An agent that writes code can be checked cheaply when the target has a formal checker. Lean provides that checker for mathematics, and a big tagged library gives agents something to build on. Teams working on AI-assisted proof, code verification or agent evaluation can use this repository as a realistic test of review pipelines: how fast can humans move code from the frontier tier into the core tier, and what do they find when they do?
For learners, it is a rare chance to read a modern, machine-checked treatment of a major field with every statement tagged to a public reference.
What is still open
- Independent confirmation of size and coverage. Neither the 16M figure nor full tag coverage has been checked by third parties in what we found.
- Review progress. How much of StacksFrontier has moved to StacksCore is not stated.
- Cost and compute. Axiom's post does not give the compute or time spent in the text we read.
- Errors found. Axiom's CFSG work reported errors in published papers; whether the Stacks work surfaced any is not stated.
We will update this post when Axiom or independent reviewers publish more.
Details reflect Axiom's X post and the GitHub repository as read on November 4, 2026. Repository contents change quickly.
Related reading
- Axiom and the Classification of Finite Simple Groups in Lean: claimed vs verified
- Lean 4 and the collapse in formal proof cost
- OpenAI math Lean RL environments on Hugging Face
- Claude, Fermat's Last Theorem and Lean
- Five open quantum problems and Lean proofs: claimed vs verified
- Boris Cherny on Opus 5.5, Lean and TLA formal verification