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.
Controlled recursion examples use the same reader: natural-number induction, a recursive family, a large shared proof. These are synthetic controls; their generation and limits are recorded separately from the two project snapshots.
Released AI-source sample: 20 complete graphs from 24 predetermined scripts, recompiled under the recorded environment. Selection, checks and limits.
Source-backed field types: selected synthetic controls, including large dependent operands. Their expression templates borrow exact source regions; the source packets still load in full.
Checked context modules: exact own-control term/type observations with separate original-use mappings. Open a source node and choose “Show checked context module”.
Paged proof geometry: the same occurrence-based notation loads source fields and native queries on demand for 34 declarations. Missing construction evidence remains explicitly marked source structure. Shared type graphs load fully within separate bounds.
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
For the two research snapshots, 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.