---
id: "2026-11-04-axiom-stacks-project-lean-formalization"
url: "https://postcutoff.com/e/2026-11-04-axiom-stacks-project-lean-formalization/"
as_of: "2026-11-09T21:13:00+01:00"
date: "2026-11-04"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 4
editor: human editor
human_review: null
version: "2026-11-09"
---

As of: 2026-11-09 21:13 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-11-04-axiom-stacks-project-lean-formalization/

# Axiom: the Stacks Project formalized in Lean

Full title: Axiom releases a 16M-line Lean formalization of the Stacks Project, mostly written by AI agents and split into human-reviewed and unreviewed tiers

Axiom Math published github.com/AxiomMath/Stacks (created 4 Nov 2026), "A Lean 4 (v4.34.0-rc2) formalization of the Stacks Project", the open reference work on algebraic geometry. The README says "We have formalized every tag of the Stacks Project with formalizable content", with declarations also tagged by EGA and SGA items. Code sits in two tiers: StacksCore, human-reviewed, and StacksFrontier, "formalizations written by AI agents", where "review is most needed". Axiom's X post called it "a 16M-line formalization of the entire Stacks Project"; two days later it released a proof of the Weil conjectures built on it.

## Key facts
- Claim (README, verbatim): 'We have formalized every tag of the Stacks Project with formalizable content'; proofs use only propext, Classical.choice and Quot.sound
- Size: about 63,000 modules (README); '16M-line' (Axiom on X, 4 Nov)
- Review status: StacksCore is 'human-reviewed … brought to Mathlib standards'; StacksFrontier is written by AI agents and needs review before moving to StacksCore. The share of each tier is not stated in the README
- Reach: Axiom's X post 'Most think vibecoding at scale is slop. Here's a counterexample. Today we release a 16M-line formalization of the entire Stacks Project…' had 6.94M views by 7 Nov (fxtwitter)
- Follow-up: AxiomMath/Weil (6 Nov), a Lean proof of the Weil conjectures built on the library (own entry)
- Contributions are taken through claimed tasks with blueprints reviewed by maintainers (README)

## What happened

Axiom Math released a Lean formalization of the Stacks Project. The 5 Nov listing had mentioned the repository only in passing; its reach (6.9M views on X) became clear on 7 Nov, so it gets its own entry. The library separates human-reviewed code from code written by AI agents and asks the community to review and promote the latter.

## Why it matters

The Stacks Project is the standard reference for modern algebraic geometry, and Mathlib covered only a small part of it. A machine-checked version, even one only partly reviewed, makes large formal proofs in the area possible: Axiom's Weil conjectures proof two days later builds on it.

## What is disputed or not yet verified

- Verification: Lean kernel-checked per the repository; agent tier not human-reviewed

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 188 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 127 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 218 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 157 days after its cutoff

## Sources

1. [AxiomMath/Stacks repository and README](https://github.com/AxiomMath/Stacks) (github.com, code)
2. [Stacks in Lean website](https://stacks.axiommath.ai/) (stacks.axiommath.ai, official)
3. [Axiom on X: release post (4 Nov)](https://x.com/axiommathai/status/2118028834515874112) (x.com, official)
4. [TechBuzz: Axiom Math verifies Stacks Project to combat AI proof slop](https://techbuzz.ai/articles/axiom-math-verifies-stacks-project-to-combat-ai-proof-slop) (techbuzz.ai, press)

## Changes

- 2026-11-09: Added TechBuzz coverage (TechCrunch's 5 Nov 'keep AI slop out of mathematics' piece covers the same story; seen only as a headline)
- 2026-11-07 (filed): Created (science agent; promoted from a passing mention in the 5 Nov listing)

## Related

- 2026-11-06: [Axiom: the Weil conjectures proved in Lean](https://postcutoff.com/e/2026-11-06-axiom-weil-conjectures-lean-formalization/index.md)
- 2026-11-05: [AI-assisted results, 5 Nov: arXiv of 5 Nov and Hexagon of 4 Nov](https://postcutoff.com/e/2026-11-05-ai-assisted-results-november-5-listing/index.md)
- 2026-10-27: [Axiom: Classification of Finite Simple Groups formalized in Lean](https://postcutoff.com/e/2026-10-27-axiom-cfsg-classification-finite-simple-groups-lean/index.md)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-11-04-axiom-stacks-project-lean-formalization/index.json