AI Proved What?

AX06 (outside OpenAI’s math catalogue), November 2026

The Stacks Project, all in Lean?

Axiom Math says it has formalized every tag of the Stacks Project with formalizable content. About 97% of the formalized tags were written by AI agents and have not yet had human review, by Axiom’s own metadata.

Play AX06: the Stacks Project in Lean. A stack of pages with the tag 09CF, and a bar that is 97% orange for the AI-written tier.

6:26. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:06The claim
  3. 2:57How the work went
  4. 5:11Where it stands

The claim, in plain words

This is AX06. The circle x² + y² = 1 passes through the point (3/5, 4/5), because 3² + 4² = 5². Algebraic geometry studies shapes like this, cut out by equations, over every kind of number system at once. Its modern foundations are vast. Since 2005, Johan de Jong has gathered them in the Stacks Project: a free online reference of roughly 7,500 pages, in Axiom’s count, written with hundreds of contributors. Every result has a permanent four-character tag. Tag 09CF, for example, is a lemma about polynomial rings.

To formalize a text is to write each definition, statement and proof in a language like Lean, whose kernel checks every step of every proof. Lean’s community library, Mathlib, already covered part of the Stacks Project. But the kernel only checks that a proof proves its statement. Whether the statement says what the book says is a separate question, and it takes a reader. Keep that in mind for this episode.

On November 4, 2026, the company Axiom Math released a blog post, a website and a public Lean repository. The README says: we have formalized every tag of the Stacks Project with formalizable content. These are statements and proofs, built on Mathlib, with no sorry and only Lean’s three standard axioms, according to the repository. Axiom’s post calls it the largest integrated, reusable library of formalized mathematics ever built. By the site’s own data, that is about 15.75 million lines of Lean, in nearly 63,000 files. It is a formalization of known mathematics: apart from corrections to the text, no new theorems are claimed. The library has two tiers. StacksCore is human-reviewed. StacksFrontier holds formalizations written by AI agents, and by our tally of the site’s data, about 97% of the formalized tags live only there.

What it doesn’t claim

What the numbers say, and what is not claimed. By Axiom’s own data, 16,219 of the 16,249 formalizable tags are counted as complete, including some where the Lean shows the printed statement fails: 14,842 in this library, and 1,377 already in Mathlib. 30 are not: 15 partial, 9 conditional, and 6 flagged as needing correction. 347 tags, mostly remarks and examples, were judged to have nothing to formalize, and the exercises are out of scope. The text followed is the Stacks Project as of April 16, 2026. And for the AI-written tier, the repository’s metadata says each statement was checked against its tag, but it has not yet had human review. The review status is self-assessed.

Where it stands

Released by Axiom
Blog post, website and repository, November 4, 2026 (the repository’s first commit, “Publication of Files”, is dated November 4 UTC; a second commit, dated November 5 UTC, fixed two files “so that lake build succeeds”). The metadata says the development took place in a repository internal to Axiom Math.
Human review of StacksFrontier
Not yet, per Axiom’s metadata: each StacksFrontier statement “was checked against its Stacks tag, but it has not yet had human review”; review status “self-assessed”. By our tally of the site’s data, about 97% of the formalized tags live only in StacksFrontier.
Independent check
None found as of November 4, 2026: no GitHub Actions runs, no comparator file, no outside build, review or expert reaction.
Peer reviewed
No (there is no paper).
Lean library, by Axiom
Lean v4.34.0-rc2 on Mathlib 16edf57; no sorry and only Lean’s three standard axioms, per the README and metadata; about 63,000 modules (README). Not built or run by us.

Last checked November 4, 2026. Where it stands. The repository’s first commit, called Publication of Files, did not build as published: by its message, a second commit, dated November 5 UTC, fixed two files so that lake build succeeds; the metadata says the development took place in a repository internal to Axiom. There are no continuous-integration runs and no comparator file, so no published check shows the library building, or pins down which statements a check would cover. The README says the library has about 63,000 modules, and that a full build takes a long time and a lot of memory. We found no independent build, review or expert reaction; the release is barely a day old. Nothing here is peer reviewed, and we did not build or run it.

Correction (November 4, 2026). The video says the repository holds a single commit. A second commit, 012108f, dated November 5, 2026 at 04:42 UTC (November 4, 20:42 Pacific), “Fix Germ.lean and DenseOpen.lean so that lake build succeeds”, changes two StacksFrontier files; by its message, Lean’s kernel rejected an equation lemma Lean generates in Germ.lean, so the first commit, f8e70c5, did not build. There are still no GitHub Actions runs and no comparator file. The numbers on this page come from the site’s data for the first commit. Not built or run by us.

This is outside OpenAI’s math catalogue, and it pairs with AX01, Axiom’s Lean proof of the classification of finite simple groups. If it holds, nearly every formalizable tag of the Stacks Project, as of April 2026, is now Lean code that the kernel accepts, with counterexamples to some printed statements; whether the AI-written tier, 97% of the formalized tags, says what the book says has so far been checked by AI, and, Axiom says, not yet by people. See AX01.

How the work went

  1. The agents. How the work went, in Axiom’s account. A hierarchical system of AI agents, designed by Axiom’s mathematicians and engineers, worked in parallel across the dependency graph: translating statements, searching Mathlib, building proofs. The repository’s metadata names AxiomProver for the autonomous part, and says the foundational definitions and StacksCore were formalized and reviewed by hand. To keep statements faithful to the text, the post describes multi-agent auditing, semantic cross-checks against the source, the requirement that each result fit the results that depend on it, and targeted audits of foundational definitions and landmark theorems. So for most of the library, matching the Lean to the book was done by AI.
  2. The repairs. Axiom also says the work surfaced dozens of statements in the Stacks Project that needed local refinement: missing hypotheses, edge cases, claims too general as stated. It publishes no list and no count. One example, from a Lean file in the repository. Tag 09CF says that on a polynomial ring you may prescribe a biderivation’s values on the variables freely. Take two variables, x and y, and let them act on a module one way from the left and another way from the right. Ask for D(x) = 0 and D(y) = 1. The product rule then gives D(xy) = 1, but D(yx) = 0, although xy = yx. Our own two-line computation agrees. The repository also calls tag 08JQ, on base change for algebraic spaces, and tag 0DS4, on dimensions of fibres for algebraic stacks, partly false as printed.
  3. The Stacks Project’s side. These are Axiom’s claims. No Stacks maintainer has confirmed them, and on November 4 the three live Stacks pages were unchanged. On October 21, de Jong asked people, for now, not to send AI-written comments or pull requests, and wrote: I intend to continue updating and fixing the Stacks project by hand. Axiom’s post says it respects that, and keeps its counterexamples and refinements in its own repository.

The numbers in the video

  • From the site’s own data (generated 2026-11-04, commit f8e70c5): 17,269 Stacks tags; 16,249 formalizable; 16,219 counted as complete (14,842 in this library, 1,377 already in Mathlib); 15 partial, 9 conditional and 6 “needs correction”; 347 judged not applicable. The site’s “complete” includes tags where the Lean shows the printed statement fails.
  • From the site’s own data: 15,751,904 lines of Lean in 62,975 files, 663,090 declarations. Axiom’s post says “some 16 million lines”.
  • Ours: of the 14,849 tags the site marks formalized, 14,423 (97.1%) have every declaration in a StacksFrontier module; 109 touch StacksCore; the rest touch Mathlib.
  • Ours: the 09CF counterexample in Axiom’s Lean file, checked by hand with the product rule D(pq) = p·D(q) + D(p)·q: with x, y acting by 1, 0 on the left and 0, 0 on the right, D(x) = 0 and D(y) = 1 give D(xy) = 1 but D(yx) = 0.
  • The Stacks text Axiom followed is commit a5811b23 of April 16, 2026 (its metadata). On November 4, 2026 the live Stacks pages for 09CF, 08JQ and 0DS4 still printed the original statements.

Read the source

AI Proved What? is independent and not affiliated with Axiom Math, OpenAI, the Stacks Project or Johan de Jong.

Transcript

Read the full script

0:00The question

This is AX06. The circle x² + y² = 1 passes through the point (3/5, 4/5), because 3² + 4² = 5². Algebraic geometry studies shapes like this, cut out by equations, over every kind of number system at once. Its modern foundations are vast. Since 2005, Johan de Jong has gathered them in the Stacks Project: a free online reference of roughly 7,500 pages, in Axiom’s count, written with hundreds of contributors. Every result has a permanent four-character tag. Tag 09CF, for example, is a lemma about polynomial rings. To formalize a text is to write each definition, statement and proof in a language like Lean, whose kernel checks every step of every proof. Lean’s community library, Mathlib, already covered part of the Stacks Project. But the kernel only checks that a proof proves its statement. Whether the statement says what the book says is a separate question, and it takes a reader. Keep that in mind for this episode.

1:06The claim

On November 4, 2026, the company Axiom Math released a blog post, a website and a public Lean repository. The README says: we have formalized every tag of the Stacks Project with formalizable content. These are statements and proofs, built on Mathlib, with no sorry and only Lean’s three standard axioms, according to the repository. Axiom’s post calls it the largest integrated, reusable library of formalized mathematics ever built. By the site’s own data, that is about 15.75 million lines of Lean, in nearly 63,000 files. It is a formalization of known mathematics: apart from corrections to the text, no new theorems are claimed. The library has two tiers. StacksCore is human-reviewed. StacksFrontier holds formalizations written by AI agents, and by our tally of the site’s data, about 97% of the formalized tags live only there. What the numbers say, and what is not claimed. By Axiom’s own data, 16,219 of the 16,249 formalizable tags are counted as complete, including some where the Lean shows the printed statement fails: 14,842 in this library, and 1,377 already in Mathlib. 30 are not: 15 partial, 9 conditional, and 6 flagged as needing correction. 347 tags, mostly remarks and examples, were judged to have nothing to formalize, and the exercises are out of scope. The text followed is the Stacks Project as of April 16, 2026. And for the AI-written tier, the repository’s metadata says each statement was checked against its tag, but it has not yet had human review. The review status is self-assessed.

2:57How the work went

How the work went, in Axiom’s account. A hierarchical system of AI agents, designed by Axiom’s mathematicians and engineers, worked in parallel across the dependency graph: translating statements, searching Mathlib, building proofs. The repository’s metadata names AxiomProver for the autonomous part, and says the foundational definitions and StacksCore were formalized and reviewed by hand. To keep statements faithful to the text, the post describes multi-agent auditing, semantic cross-checks against the source, the requirement that each result fit the results that depend on it, and targeted audits of foundational definitions and landmark theorems. So for most of the library, matching the Lean to the book was done by AI. Axiom also says the work surfaced dozens of statements in the Stacks Project that needed local refinement: missing hypotheses, edge cases, claims too general as stated. It publishes no list and no count. One example, from a Lean file in the repository. Tag 09CF says that on a polynomial ring you may prescribe a biderivation’s values on the variables freely. Take two variables, x and y, and let them act on a module one way from the left and another way from the right. Ask for D(x) = 0 and D(y) = 1. The product rule then gives D(xy) = 1, but D(yx) = 0, although xy = yx. Our own two-line computation agrees. The repository also calls tag 08JQ, on base change for algebraic spaces, and tag 0DS4, on dimensions of fibres for algebraic stacks, partly false as printed. These are Axiom’s claims. No Stacks maintainer has confirmed them, and on November 4 the three live Stacks pages were unchanged. On October 21, de Jong asked people, for now, not to send AI-written comments or pull requests, and wrote: I intend to continue updating and fixing the Stacks project by hand. Axiom’s post says it respects that, and keeps its counterexamples and refinements in its own repository.

5:11Where it stands

Where it stands. The repository holds a single commit, called Publication of Files; the metadata says the development took place in a repository internal to Axiom. There are no continuous-integration runs and no comparator file, so no published check shows the library building, or pins down which statements a check would cover. The README says the library has about 63,000 modules, and that a full build takes a long time and a lot of memory. We found no independent build, review or expert reaction; the release is barely a day old. Nothing here is peer reviewed, and we did not build or run it. This is outside OpenAI’s math catalogue, and it pairs with AX01, Axiom’s Lean proof of the classification of finite simple groups. If it holds, nearly every formalizable tag of the Stacks Project, as of April 2026, is now Lean code that the kernel accepts, with counterexamples to some printed statements; whether the AI-written tier, 97% of the formalized tags, says what the book says has so far been checked by AI, and, Axiom says, not yet by people.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.