Expression
Proof Atlas / Visual language
Read Lean.
See its structure.
From readable source to checked terms: explore the parts of Lean, how they connect, and what each picture can tell you. Every entry pairs a small example with a diagram, an explanation and its source.
Reference baseline: Lean 4.33.1. All 12 Expr, 6 Level and 4 Syntax constructors; major families of surface terms, tactics, commands and macros; selected elaborator structures. Lean is extensible: this is a scoped reference, not a claim to list every library notation or tactic.
01 / Four scales, with explicit evidence
One proof. Four ways to see it.
02 / Language reference
Different layers. Different links.
03 / Beyond the kernel
Lean code is larger than `Lean.Expr`.
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.
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.
Small trusted language
Γ ⊢ p : PThe kernel checks expressions using declaration environments and trusted rules. Some expressions also contain metadata or projections. The diagrams illustrate constructors, not every typing judgment. Universes, local contexts and declaration kinds are separate structures.
View boundaries
(inputs) ──[proof]──▶ (result)A collapsed graphic must retain assumptions, binder scope, axiom dependencies and a link to evidence. The SE(2) viewer exposes structural provenance; semantic compression still requires checked contracts.
← Explore the measured SE(2) Lean proof · Compact Expr catalogue · Read the research result · Lean Expr API reference