Proof Atlas / Visual manual · notation revision 1

Reading the geometry of a Lean proof

The drawing starts from an expression occurrence, its ordered fields and its binding context. Larger figures compose these objects into applications, introductions and local definitions. This manual explains what each connection means, what folding preserves, and where the language remains incomplete.

The interactive examples below are authored structural controls. They use the production scene model, but have no native typing certificate. Links to recorded compiled proofs are provided separately.

1. Read the relation before the shape

Solid / field: an ordered expression child. The label names its constructor port.
Dashed / bound-to: a variable refers to its lexical binder. It is not another child.
Dotted / attribute or reference: a name, level, metadata value or context identifier. Read the explicit relation label.
Rule bar: premises and conclusion of a typing judgment. Native evidence is required for an instantiated checked rule.

The source viewer also has frontier ports: a retained root with hidden descendants and an exact count. An external Γ boundary identifies a binder outside the cut. Neither means “missing proof”. Position and distance carry no mathematical meaning. Existing specialist views use their own labelled layouts; the key describes relations, not a metric embedding or a new proof calculus.

source identity = packet hash + root + ordered child route
computed identity = evidence/derivation hash + namespace + computed route

A stored DAG node may occur more than once, under different binders. Select an occurrence route, not just a node number. A type or substitution result has its own namespace; it does not acquire a source location merely by looking similar.

2. Inspect scope, then change scale

Select an occurrence to inspect its original path and outgoing fields. For a bound variable, follow its binder. Focus a subtree to move that binder outside the cut. Toggle folding and depth to check the accounting identity.

Example Depth Fold binders and applications

Scroll to pan. Nodes support Tab and Enter.

3. The complete expression alphabet

These are the twelve semantic Lean.Expr forms in the pinned exporter. Every semantic field is listed in constructor order. Solid connectors are Expr children; other fields retain their declared relation. domain in exported routes is the display alias for binderType. Cached implementation data are excluded.

Field definition: Lean v4.33.1 Expr.lean. A constructor shape alone supplies no inferred type.

Loading the pinned field catalogue. The language reference provides the full schema and surface-language families.

4. Composition without losing the term

Ordered binder telescope Tₙ

$$\begin{gathered}\underbrace{\lambda (x_1:A_1)\ldots\lambda(x_n:A_n),\,t}_{n\text{ retained binders}}\\\longmapsto\quad T_n\,[x_1:A_1,\ldots,x_n:A_n]\ ;\ t\end{gathered}$$

Retain each binder's original route, kind, visibility and header regions. Headers use the context before their binder; the continuation sees the extended context. The same rule can retain mixed lam, forallE and letE prefixes. A folded forallE remains a type binder.

Application spine @ₙ

$$\begin{gathered}(((h\,a_1)\,a_2)\ldots a_n)\\\longmapsto\quad\mathbin{@}_n(h; a_1,\ldots,a_n)\end{gathered}$$

Keep all original application occurrences and arguments in order. head and argN are abstract ports. Grouping performs no substitution, hides no implicit argument and proves no saturation or logical inference. A capped spine explicitly retains the remaining function region.

Exact cut and frontier

$$N_{\mathrm{retained}}+\sum_{R\in\mathcal F}|R|=|t|$$

A large count is stored exactly. Expanding a frontier refines one region while preserving the selected root and its scope interface. Counts measure syntax occurrences, not proof difficulty, premise necessity or time to understand a proof.

Shared terms, separate occurrences

$$\begin{gathered}e_k\text{ at }r_1\text{ in }\Gamma_1\\ e_k\text{ at }r_2\text{ in }\Gamma_2\end{gathered}$$

Storage sharing does not merge lexical meaning. A source reference or context module keeps its own provenance and explicit original-use mapping. Computed substitution must avoid capture; descendants do not inherit a new native judgment.

Syntax-use counts and native recorded-use counts answer different questions. The first counts occurrences in the complete stored body. The second counts the finite native observations retained in an evidence package. A syntactically unused binder is not a proof that an assumption is mathematically unnecessary.

5. From syntax to a checked construction

Read $\Gamma\vdash t:A$ as “in context Γ, term t has type A”. The schemata below explain the notation; each concrete viewer instance needs a matching recorded judgment. $\equiv$ denotes definitional conversion, distinct from structural identity and a proof of equality.

Π application

$$\frac{\begin{gathered}\Gamma\vdash f:\tau\quad\tau\equiv\Pi(x:A),B\\ \Gamma\vdash a:A'\quad A'\equiv A\end{gathered}}{\Gamma\vdash f\,a:\tau'\quad\tau'\equiv B[a/x]}$$

The argument type is compared with the expected domain; the result is instantiated in order. Proof/type/value roles come from recorded type information. A proof argument may become a premise, while a value argument remains a parameter.

Lambda introduction

$$\frac{\Gamma\vdash A:\operatorname{Sort}u\qquad\Gamma,x:A\vdash t:B}{\Gamma\vdash(\lambda(x:A),t):\Pi(x:A),B}$$

The domain is outside x's scope; the body is inside. The interface discharges x at the conclusion. It is an implication introduction only in the appropriate propositional case.

Local definition

$$\frac{\begin{gathered}\Gamma\vdash A:\operatorname{Sort}u\quad\Gamma\vdash v:A\\ \Gamma,x:A:=v\vdash t:B\end{gathered}}{\Gamma\vdash(\mathbf{let}\ x:A:=v;\ t):B[v/x]}$$

The type and value precede the binder. The body sees both its type and value. Native records may expose separate type-conversion and computed substitution views; their roots and evidence remain distinct from source routes.

Elimination and recursive premises

$$\frac{\begin{gathered}\text{parameters, motive, branch methods}\\\text{indices, major premise}\end{gathered}}{\text{recursor application}:\text{instantiated motive}}$$

A recursor needs its actual signature, constructor fields and branch contexts. This is an interface sketch, not a universal recursor typing rule. Recorded cases and recursive premises have dedicated views; arbitrary recursors and every tactic strategy are not covered by a complete automatic interpretation.

A native extraction record ties a finite judgment to a specific environment, packet and context. The browser validates that identity; it does not run Lean. An article correspondence is a separate reviewed relation and is not implied by a typing rule.

6. Universes and the boundary with source syntax

Level.zero          0
Level.succ u        u + 1
Level.max u v       maximum of u and v
Level.imax u v      0 when v = 0; otherwise max u v
Level.param n       named universe parameter
Level.mvar id       unresolved universe metavariable

Universe edges form a separate level graph attached to sort and const. They are not term-child ports or de Bruijn binder links. $\operatorname{Prop}=\operatorname{Sort}0$ and $\operatorname{Type}u=\operatorname{Sort}(u+1)$. See the pinned level definition and layered Lean reference.

Layer	Examples	What the geometry can recover
Kernel expressions	All 12 forms above	Ordered structure, payloads, exact occurrence routes and lexical scope.
Surface terms	Notation, `fun`, `match`, `do`, coercions	The elaborated expression, when exported. Original spelling and desugaring history need source maps.
Tactics	`intro`, `simp`, `aesop`, `omega`	The resulting term; the final term does not uniquely reconstruct the tactic execution.
Commands and macros	`theorem`, `def`, `inductive`, syntax extensions	Exported declarations and environment relationships. No complete command/macro execution trace.
Elaborator state	Goals, local contexts, assignments	Only explicitly retained records. An unresolved metavariable is not an accepted closed proof.

7. What the language can currently do

This is an evidence-based assessment by task, without a numerical “power” score. Structural correctness, useful abstraction and human comprehension require different tests.

Task	Supported result	Weakness / next test
Recover syntax and binding	All 12 constructor forms; 6,166 audited cuts over the 2,098-packet inventory; 4,972 checked lexical links. Evidence.	These are serialized representation checks. They do not independently rebuild every original proof.
Inspect a very large term	The recorded largest body has 462,476,271 expanded occurrences. A composed initial cut has 21 vertices with exact retained/hidden accounting. Evidence.	Access is bounded; useful semantic compression and comprehension are unmeasured. Paged source delivery covers 35 profiles, not all 2,118 count profiles.
Follow assumptions to uses	152 public indexed variable uses in 26 profiles, with exact binder/context/type links; syntax counts cover 44,887 stored binders in 2,118 packets. Use evidence · Count evidence.	Native observations are sparse and differ from complete syntactic occurrence counts. No premise-necessity conclusion.
Read a proof construction	Recorded applications, introductions, local definitions and selected recursor/constructor/projection cases retain typed interfaces. Evidence.	A generic automatic semantic notation for arbitrary elimination and proof strategy remains incomplete.
Inspect AI-source proofs	A frozen attributed sample is included separately from project proofs. Dataset and limits.	It does not establish performance or comprehension across massive AI-generated proofs.
Learn the notation	This manual and the corrected field diagrams expose every semantic field, including all three `letE` children. The scope lab uses the existing scene model.	Browser and schema tests measure faithful presentation. A timed study of scope tracing, premise finding and error localization remains necessary.

Improvement in this iteration: the old constructor gallery used a generic two-input picture. It omitted fields and blurred child/reference roles. The gallery and this manual now share a field-driven renderer, explicit relation labels and pre-/post-binder contexts. The interactive controls expose the shared-node/different-binder counterexample and exact folding identities. No new semantic or comprehension claim follows.

8. Use the notation on recorded proofs

Lemma 3.2 / Riccati bound: inspect an introduction or local definition, then select a recorded use and follow its original binder. Count provenance is a separate annotation.
Positivity proof: compare raw syntax, folded telescopes and grouped application spines. Use source routes to return to the same occurrence.
Large compiled proof: inspect the finite frontier rather than expanding the complete occurrence tree.

At an unrecorded path, keep the structural view and the explicit “not queried” state. It must not inherit the enclosing node's type evidence. For source alignment, use the synchronized article reader; unsupported passages remain marked separately.

Reproduction: schema and scope/partition checks · browser checks · research program. The general language and its evaluation remain work in progress.