Proof Atlas / Visual language

The anatomy of a Lean expression

A formal proof is not a forest of unnamed dots. Each expression node has a constructor, typed connections and a precise role. Select a glyph to see its shape, its inputs, and a short Lean example.

Complete at the kernel constructor layer: all 12 `Lean.Expr` variants. Not a claim of complete Lean surface syntax: notation, commands, macros, tactics, and attributes elaborate into this core (or act on declarations and environments). These require additional layers.
01 / Four scales, with explicit evidence

One proof. Four ways to see it.

01 · CertificateΓ ⊢ proof : Papp (const ...) (lam ...) (bvar 0)Kernel-checked expression 02 · Typed graphEvery typed expression link 03 · Collapsed moduleLemma Lopen to inspectInputs and result retained 04 · Mathematical ideaExistenceUniquenessExactly oneAnnotated, not automatic
02 / The kernel alphabet

All twelve `Lean.Expr` constructors

These are the closed set of constructor tags defined by Lean 4's `Expr` type. The drawings below encode syntactic links; they are not claims that arbitrary node positions have mathematical meaning.

Core expression

app — Function application

Lean example


            
How to read the picture

          

        

      

    

  

  

    
03 / Beyond the kernel

    
Lean code is larger than `Lean.Expr`.

    

      
Surface language
Readable notation
theorem t : A ∧ B := ⟨ha, hb⟩
Tokens, declarations, names, syntax quotations, notation and macros belong to a richer syntax tree. They are not additional kernel `Expr` constructors.

      
Elaboration
Resolve and elaborate
by simp [h]
Tactics and elaborators use goals, contexts, metavariables, type-class synthesis and elaboration information to construct terms. Their execution history is not preserved by a bare final proof term.

      
Kernel
Small trusted language
Γ ⊢ p : P
The kernel checks expressions using declaration environments and trusted rules. Some expressions also contain metadata or projections. The diagrams illustrate constructors, not every typing judgment.

      
Proof Atlas
Certified view contracts
(inputs) ──[proof]──▶ (result)
A collapsed graphic must retain assumptions, binder scope, axiom dependencies and a link to evidence. Our SE(2) viewer currently proves graph provenance, not universal semantic compression.

    

    
Next formal milestones: graphical inference rules for application/binders, correct de Bruijn scope links, shared declarations, definitional equality and transport, recursors/induction, classical assumptions and quotient constructors. We must test each rule on a kernel-checkable example before extending the vocabulary.

    
← Explore the measured SE(2) Lean proof · All 12 rules in one illustrated catalogue · Read the research methodology · Lean Expr API reference