The Stacks Project, Formalized in Lean
namanbnsl
79 points
23 comments
November 05, 2026
Related Discussions
Found 5 related stories in 133.5ms across 11,756 title embeddings via pgvector HNSW
- Are We Stuck with Lean? jjgreen · 135 pts · July 30, 2026 · 58% similar
- Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem jsLavaGoat · 12 pts · September 26, 2026 · 57% similar
- AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura datascientist · 11 pts · October 29, 2026 · 55% similar
- OpenAI’s Navier-Stokes release included a Lean 4 formal proof ibobev · 153 pts · September 10, 2026 · 54% similar
- The Double Headed Stack Allocator g0xA52A2A · 43 pts · October 15, 2026 · 53% similar
Discussion Highlights (8 comments)
eternauta3k
Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?
breezybottom
The fact that the description is AI slop doesn't inspire confidence in the results.
QuesnayJr
After they announced the formalization of the classification of Finite Simple Groups, I immediately wondered "What would happen if you tried to formalize the Stacks Project?" Despite also being very long, it's the opposite of the CFSG: instead of a poorly organized set of results that contribute to proving one big theorem, it's instead a carefully-organized set of results that cover a broad area. The Stacks Project was the model for how mathematics should be done (at least for the pre-LLM era). Algebraic geometry had lots of poorly organized foundational results that were not really created for themselves, but in order to solve problems in the field. One person, Aise Johan de Jong, set out to fix it by organizing a project to write out the proofs of all of the results in a carefully organized fashion. He's led the project since, though of course there are multiple contributors. The whole thing is thousands of pages. I would be interested in hearing more about the gaps they uncovered in the existing results, and how they fixed them.
vatsachak
Okay this is actually useful AI formalization. But the stacks project is basically Lean in natural language anyways, so it makes sense why its high quality.
AlexCoventry
Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)
jptlnk
Kind of ironic that (as of today) the most recent blog post from Oct 21 '26 on the original Stacks Project is "21 Oct 2026: No AI for now" A very good friend of mine is an algebraic geometer and all of the AI progress in math is, to put it mildly, bumming him out. And me too honestly! I understand the allure of doing this kind of work in AI on some level, but I'm becoming increasingly skeptical of generating "knowledge" that's difficult or impossible for humans to understand (at scale or otherwise).
nhatcher
Related: https://news.ycombinator.com/item?id=40025362
throw567643u8
Why would mathematicians want to build upon a corporate product? It's against the principles of free and open academic research.