PROOF ATLAS / COMPLETE PROOF LIBRARY
Compiled Lean library
Browse the compiled declaration inventory, complete compiled proof terms, shared expression graphs and exact declaration references. The optional scoped geometry prototype uses constructor glyphs, ordered ports and occurrence-specific binder links; collapsed descendants retain exact accounting.
Select a declaration
Visible scoped occurrences and boundaries
Each row identifies an occurrence path, rather than merging shared nodes. Collapsed descendants remain recoverable from their packet and route. λ/∀/let have separate domain, value and body ports; dashed links identify lexical binders. This prototype does not infer the type of every expression.
Every declaration in this edition
What the inventory proves
Module ownership is the denominator: every project declaration, every complete type, every available theorem or definition body, and recursor reduction rules are included. Every compiled type, proof body and elaborated child link remains available. Original source projects and tactic scripts remain private. Shared subterms are stored once; exact expanded occurrence counts are computed without unfolding the graph. Large branches are collapsed visually and can be opened by their node number.
Article links identify a reviewed proof or supporting-module context. They do not certify that every article sentence follows from Lean. Lean/Mathlib dependencies outside this project remain named external boundaries. Surface syntax, tactics, macros and elaborator state are distinct from the twelve kernel expression constructors; the kernel diagram represents elaborated terms.