Axiom: the Stacks Project formalized in Lean
Awaiting review
Importance: major (4 of 5)The takeaway
On 4 Nov 2026 Axiom Math released AxiomMath/Stacks, a Lean 4 formalization of ‘every tag of the Stacks Project with formalizable content’ (about 63,000 modules), with an agent-written StacksFrontier tier and a human-reviewed StacksCore tier. Axiom’s X post had 6.9M views.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 9 November 2026
Your AI and this story
- GPT-6 Astra188 days after its cutoff
- Claude Opus 5.5127 days after its cutoff
- Gemini 4 Argon218 days after its cutoff
- Grok 4.7157 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 127 days before 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 |
|---|
Sources
4 sources from 4 sites. Numbers match the chips in the text.
4 sources: 3 primary, 1 press
Primary
- AxiomMath/Stacks repository and READMEgithub.com, code
- Stacks in Lean websitestacks.axiommath.ai, official
- Axiom on X: release post (4 Nov)x.com, official
Press
- TechBuzz: Axiom Math verifies Stacks Project to combat AI proof sloptechbuzz.ai, press
Changes
- Added TechBuzz coverage (TechCrunch’s 5 Nov ‘keep AI slop out of mathematics’ piece covers the same story; seen only as a headline)
- Filed (science agent; promoted from a passing mention in the 5 Nov listing)