Report: 97% of Axiom's Stacks Tags Await Review

What was released

The Stacks Project is the closest thing algebraic geometry has to a single, self-contained foundation: an open-source reference, started by Johan de Jong in 2005 and built by hundreds of contributors, in which every definition and theorem carries a permanent four-character tag and every assumption is stated. Axiom's release translates that text into Lean, the proof assistant whose kernel checks each proof step mechanically, as one library built on Mathlib. Axiom calls it, in its own words, the largest integrated, reusable library of formalized mathematics ever built. That superlative is the company's. The scale underneath it is not in dispute: roughly 7,500 pages in, some 16 million lines out.

The coverage has a boundary. The repository says it formalizes every Stacks tag with formalizable content; examples, exercises and remarks not yet formalized remain open tasks for contributors. "Entire Stacks Project" describes the scope of the formalization, not a literal translation of every item on every page.

The point of doing this to a reference work, rather than to a single theorem, is reuse. A researcher, human or agent, formalizing a new result about curves can import Stacks definitions instead of rebuilding the foundations of schemes and cohomology first, and the kernel will enforce that each imported result is applied only where its stated hypotheses hold. Axiom did the single-theorem version of this a week earlier, with the Classification of Finite Simple Groups. This is the library version, and its value depends on a different property: not whether one proof checks, but whether thousands of statements say what they are supposed to say.

Two tiers, and where the tags sit

Axiom is candid about the structure, and the candor is on its own site. The library, called Stacks, has two parts. StacksCore is code that a person has checked against the Stacks Project and brought up to Mathlib standards of naming, generality and style. StacksFrontier is code written by AI agents that has not had that review yet. The repository README makes the same distinction and adds the line that matters: every proof in either tier is kernel-checked; the tiers differ in who has reviewed the code.

On 6 November, TechTimes reported that an analysis of the project's published metadata, by AI Proved What?, put about 97% of the formalized tags in StacksFrontier. Read carefully, that figure is about review status, not correctness. A tag in Frontier is not necessarily a wrong proof. Its Lean proofs are kernel-checked, but the formalization has not yet received the human review against the original Stacks text that is required for promotion into StacksCore. The analysis itself, as TechTimes noted, had found no independent build verification as of 4 November, and its authors had not built or run the library themselves. Both cautions belong next to the number.

What the kernel does and does not check

This distinction is the whole story, and it is not a technicality. Lean's kernel verifies that a proof follows from a formal statement. It has no access to the informal English, or French, or mathematical intent on page 4,000 of the Stacks Project. If an agent formalized a slightly weaker statement than the original, or a stronger one with an extra hypothesis quietly added, the kernel will still certify the proof, because the proof is genuinely a proof of the statement as written. Axiom knows this: its blog post says ensuring each formal statement faithfully captures the original text is even more important than verifying its proof, and describes multi-agent auditing and semantic cross-checks against the source as its answer.

That answer is a process claim, and like every process claim it will be settled by sampling and reuse, not by assertion. The first outside sampling has started. TechTimes reported that Mathlib maintainer Kim Morrison, in a 5 November post, welcomed the release while pointing to duplicated formalization work, gaps between some Stacks statements and their formalized counterparts, and issues that could affect reuse. Those observations are known here through TechTimes' account, not an independent examination of Morrison's original post. None of that makes the library invalid. It locates the remaining work exactly where the tier names say it is: in the reading.

Axiom's own findings cut in its favor here, and they are worth stating plainly. The same pipeline that produced Frontier also surfaced dozens of statements in the original Stacks Project that needed repair, including missing hypotheses and claims that failed at the generality stated, and formalized corrected theorems alongside counterexamples. A system that catches errors in a twenty-year-old human reference is not merely transcribing. But catching errors in the source and mistranslating the source are compatible activities, sometimes in the same file, which is why the human review tier exists.

The practical costs nobody puts in the headline

Two details in the repository deserve more attention than the line count. The library has about 63,000 modules, and the README warns that a full build takes a long time and a lot of memory. Mathlib's own compiled files can be downloaded with `lake exe cache get`, but there is no equivalent cache for the compiled Stacks modules themselves; a cache service for them is planned rather than available. Independent verification, the property that is supposed to distinguish formalization from assertion, is therefore expensive to exercise today: anyone can check the proofs, in the sense that anyone with substantial compute and patience can. The second detail is encouraging by contrast. The README states there is no `sorry`, Lean's placeholder for an admitted gap, and no `native_decide`, and that proofs rest only on the three standard axioms. These are specific repository claims that an outside reviewer can inspect and test mechanically. They are more useful than an unsupported assurance that the proofs are sound, although the desk has not independently built the full library to reproduce them.

There is also a boundary Axiom handled correctly. On 21 October, de Jong asked that AI-generated comments and pull requests not be submitted to the upstream Stacks Project for the time being. Axiom kept its formalization, counterexamples and refinements in its own repository, under its own site, and said so. The original text remains a human project; the machine-checked shadow of it lives next door, clearly labeled by tier.

Sources

[1] Axiom, "The Stacks Project, formalized in Lean", 4 November 2026 (read in full first-hand; release claim and scale, agent-swarm description, faithfulness auditing description, dozens of statements needing refinement, de Jong 21 October boundary)Read source
[2] Axiom, Stacks Project in Lean, project site (tier definitions: StacksCore as code a person has checked against the Stacks Project, StacksFrontier as AI-written code that has not had that review yet, Lean checks every proof in both)Read source
[3] AxiomMath/Stacks, public GitHub repository README and formalization.yaml (read first-hand; created 2026-11-04T05:03:55Z; Lean 4 v4.34.0-rc2 per the README; every tag with formalizable content; no sorry and no native_decide; standard axioms only; about 63,000 modules; full build takes a long time and a lot of memory; Mathlib cache downloadable via lake exe cache get, cache service for the compiled Stacks modules planned; review status self-assessed; Apache 2.0)Read source
[4] AI Proved What?, entry AX06 on Axiom's Stacks Project formalization (read first-hand; 16,219 of 16,249 formalizable tags counted as complete by Axiom's own data; about 97% of the formalized tags written by AI agents and not yet human-reviewed)Read source
[5] TechTimes, report on Axiom's Stacks formalization and its review tiers, published 6 November 2026 at 15:09 UTC (AI Proved What? metadata analysis putting about 97% of formalized tags in StacksFrontier, with its no-independent-build-verification caveat dated 4 November; summary of Kim Morrison's 5 November post)Read source
[6] SeaPRwire, "Axiom Math Puts 7,654 Pages of Mathematics Through a Machine Checker", 5 November 2026 (TechCrunch reporting carried by SeaPRwire gave 7,654 pages)Read source
[7] ALFW, "Axiom's Agents Checked the Enormous Theorem. They Also Found a Hole in It.", 27 October 2026 (our own earlier coverage of the separate CFSG release, used only for the contrast)Read source

THE ALFW VERDICT

The achievement is real, and so is the asterisk, and Axiom, to its credit, printed the asterisk itself in the tier names. Some 16 million lines of kernel-checked Lean is a genuine engineering result, the no-placeholder and standard-axioms claims are properly checkable, and the corrections to the source text show the pipeline doing more than copying. What has not happened yet, for about 97% of the formalized tags on the reported count, is the slower human work of confirming that the formal statements are the statements Stacks actually makes. Until that review moves, or outside groups build on Frontier code and report where it breaks, describe this as a machine-checked formalization of extraordinary scale, with most of its statements still awaiting human review. That is already a significant engineering achievement. It is not the same thing as a fully human-validated mathematical foundation.