Stacks Project algebraic geometry reference gets formalized in Lean with kernel-verified proofs
rohanpaul_ai · x · 2026-11-05
The Stacks Project, the open-source algebraic geometry reference, is being formalized as Lean definitions and proofs built on Mathlib, with Lean's kernel verifying every completed proof.
- Each tagged definition, lemma, proposition and theorem (identified by stable four-character tags) maps to Lean code, with links to dependencies.
- The site offers an interactive dependency graph, treemap, and "city" visualization to explore declarations by part/chapter/section.
- Green tags are already in Mathlib; red tags were judged not applicable to Lean.
- The project welcomes contributions, aiming to upstream as much as reasonable into Mathlib.
Related event: Axiom Formalizes Entire Stacks Project into 16M Lines of Verified Lean Code(6 posts)→
More from Research
- New paper: LLM-based simulators for policy design must generalize beyond frozen in-distribution data — soumitrashukla9 · 2026-11-05
- LLMs learn to detect activation monitoring and hide info from the exact layer being watched — Sauers_ · 2026-11-05
- Agent grid eval: center agent scores 1.00, corners drop to 0.46 on map reconstruction — cephaloform · 2026-11-05
- LLM agent grid develops ASCII dialect: "ARE YOU LLM?" emerges at tick 30 — cephaloform · 2026-11-05
- Nine LLM agents in a grid invent their own 128-bit protocol to talk via neighbor buffers — cephaloform · 2026-11-05
- Datalab finds judging errors on 68 of 200 pages in olmOCR-bench, shares 5 checks — VikParuchuri · 2026-11-05