01 / CORE
Expression constructor
.app fn arg
Kernel-level constructor fields. A source example is illustrative; the type checker validates the complete expression.
Proof Atlas · The core language
Twelve ways to build
a Lean expression.
What the kernel sees is not a paragraph of tactics. It is a typed expression built from twelve constructor forms. Here is the complete structural alphabet our CoreGIR exporter handles, each with its ordered semantic fields, a Lean example, and its limits.
Three different languages must not be confused
01 / AUTHOR
Lean source
theorem, def, by, pattern matching, tactics, notation and macros. Rich, expandable syntax.
02 / ELABORATE
Core expression
Applications, binders, constants, projections, literals, metadata and references. Twelve constructors, formal scope.
03 / VERIFY
Kernel
Checks a term has its expected type in an environment. Drawings are explanatory views, not substitutes for checking.
The complete CoreGIR constructor vocabulary
Every node has a rule.
Select a form to explore its inputs, output, binding behavior and examples. The coloring indicates abstract syntax roles—not theorem truth values. Six forms were observed in the exported SE(2) benchmark; the other six are part of the universal exporter.
Loading the Lean expression visual grammar…
What this does—and doesn't—claim
These diagrams provide a proposed visual grammar for the complete Lean.Expr constructor algebra. They do not yet constitute a certified translation of the entire Lean surface grammar, a tactic-language visualizer, or a proof-net calculus for every theorem. Terms still need typed boundaries, references and environments; scope cannot be inferred from mere visual proximity.
The initial research benchmark publishes the structure and exported term payloads of CrossingData.crossing. The Lean.Expr reference and our exhaustive CoreGIR exporter define the scope of the twelve rules.
Illustrative views of a kernel expression
03 / A precise visual language
Change the scale.
Keep the evidence.
The diagram vocabulary begins with the twelve actual Lean kernel expression constructors. Each has ordered fields and a visual role. The same proof can then be seen as a full syntax graph, a collapsed module with its context preserved, or a mathematical explanation linked back to the checked term.
All twelve constructor forms · six observed in CrossingData.crossing
A visual reference, not a universal automatic proof interpreter.
Selected expression form
app · Application
Lean applications connect a function expression to an argument expression.
02 / GRAPH
Typed connections
An expression graph distinguishes child expressions from references.
03 / MODULE
Preserved boundary
A collapsed module must preserve external assumptions and evidence.
04 / IDEA
Mathematical interpretation
The full theorem context is needed to interpret the mathematical reasoning.
The proposed diagrams are not proof certificates.
SOURCE SYNTAX
theorem · def · by · match · notationRich, extensible syntax. A tactic script is not a single additional kernel expression constructor.
ELABORATION
goals · metavariables · local contextElaborators and tactics construct checked terms; their execution history is not fully retained by a final certificate.
THEOREM / PROOF
Γ ⊢ proof : PropositionValidity comes from the kernel checking a well-formed term against a type in an environment.