Exact certificate
Lean checks an expression against a type in a context. The underlying formal object—not the drawing—is the source of proof validity.
Research program / Proof Atlas · 2026
Can a proof
have a shape?
A Lean proof is an exact mathematical object. What happens when we stop reading it as thousands of symbols and begin to explore it as a landscape—branches, junctions, repeated forms, and the ideas that hold everything together?
7,288expression occurrences
7,286structural edges
431binder references
42distinct direct dependencies
01 / A new way of looking
Not a picture of mathematics.
A picture of the proof.
Formal verification gives a proof a precise structure: terms, types, declarations, binders, and applications. Our first view treats these as a graph. Each visible point belongs to an expression occurrence in an actual Lean certificate; the edges record how the expression is assembled.
But a syntactic graph is not the same thing as an explanation. A theorem may contain thousands of repeated type expressions while resting, mathematically, on a single clever argument. Proof Atlas keeps these two levels distinct—and aims eventually to connect them without losing rigor.
02 / Interactive research instrument
Inside a real Lean proof
A measured, anonymized structural projection of CrossingData.crossing (SE(2) crossing lemma). No unpublished Lean proof term is served to the browser.
Whole-proof geometryExpression occurrence forest · measured structure
7,288 expression occurrencesSelect a node to inspect
↗
Exact versus interpretive. Whole proof and recursion use observed CoreGIR syntax. The dependency view uses actual reference counts but anonymizes some names. The mathematical-idea view is a human-authored interpretation of two named supporting lemmas—not automatically inferred from graph topology.
03 / Four representations, one object
Change the scale.
Keep the evidence.
Structural anatomy
Applications, variables, binders, shared references. Graphs reveal syntax reuse and branching; their layout is a choice.
Fractal navigation
A visible branch can open into another subgraph. Its boundary must preserve every externally required premise.
Mathematical reading
Continuity and endpoint coverage establish existence; monotonicity and endpoint gluing establish uniqueness. This interpretation is currently annotated.
04 / What the experiment establishes
We can see the syntax.
Can we see the idea?
Measured. The export contains 7,288 occurrences, 7,286 child edges, 431 links from bound-variable occurrences to their binders, 2,892 constant-use occurrences, and 42 distinct directly referenced declarations. Its maximum expression depth is 49 edges.
Exploratory. Structural fingerprinting found 665 different subtree fingerprints among 7,288 occurrences. That is repetition of syntax patterns, not proof equivalence, semantic redundancy, or a safe invitation to merge nodes across different binding contexts.
Open. This prototype does not expand the internal proof bodies of every referenced lemma and does not discover the core argument automatically. The next test is to include transitive local proofs and see whether their logical modules can be recovered faithfully.
05 / Read and reproduce
The research trail
Research introductionFrom certificates to geometric explanations ↗Motivation, diagram grammar, claims and falsifiable next tests
Public structural dataAnonymized graph projection ↗Real 7,288-node topology; no private certificate payload
External referenceThe Lean 4 reference manual ↗Kernel expressions, proofs and dependent type theory