Explore the interactive proof graph →
Imagine a hundred-page mathematical argument. At ordinary reading scale it is a succession of definitions, estimates, lemmas and proofs. From a distance we may instead see a single structure: long chains of implications, shared pillars, branches that rejoin, bottlenecks, and regions whose internal reasoning repeats. Does a formal proof have a meaningful geometry, and can that geometry help us understand its mathematical idea?
Lean provides an unusually good starting point because its kernel checks a proof as an expression with a type. It does not accept a diagram merely because the diagram is persuasive. Formally, in a context of assumptions and declared objects $\Gamma$, the assertion
\[\Gamma \vdash p : T\]means that $p$ is a proof term whose type is the proposition $T$. Lean expressions are constructed from applications, binders, constants and other precisely defined constructors. See the Lean expression reference and Theorem Proving in Lean 4.
The experiment is to begin with that checked object, recover its connections, and then ask what is lost or gained as we choose increasingly abstract representations.
Two geometries—and why they must not be confused
A structural graph represents the syntax and references of the formal object. In our initial benchmark a node is an occurrence of a Lean expression, a structural edge joins it to a subexpression, and additional links point a bound variable to its binder or a constant occurrence to its declaration.
A mathematical explanation is a different object. It may say that continuity establishes existence, monotonicity establishes uniqueness, and the combination yields exactly one crossing. Those statements reveal mathematical meaning, not merely the nesting of applications and binders.
There is no reason for the most central syntactic node to be the most important idea. The type Real can occur hundreds of times even though a theorem’s essential insight may be a single interval-covering argument.
The project therefore treats the proof as one exact object with several distinct views:
| Scale | Visible structure | What it can legitimately tell us |
|---|---|---|
| Exact syntax | Expressions, binders, constructors | How the checked term is assembled |
| Dependency graph | Named declarations and their uses | Which results and objects the theorem references |
| Recursive modules | Expandable subarguments with typed boundaries | How pieces of the proof compose, if the boundaries are preserved |
| Explanation | Existence, uniqueness, contradiction, induction, geometry | A mathematical interpretation, which must retain provenance to be trustworthy |
These views need not all be generated automatically. In the present prototype the first two follow from measured exports; the explanatory grouping is explicitly authored and labeled.
Why borrow from Feynman diagrams?
The useful analogy is local graphical composition. In a Feynman diagram, permitted lines and vertices have mathematical meanings and composition rules. The diagram is not, in general, a drawing of a particle’s most probable actual path; individual diagrams represent contributions to perturbative calculations. We want to borrow the discipline of a small visual grammar, not the probability interpretation.
A mathematical proof may likewise be represented through ports (inputs and outputs), wires (uses or dependencies), interaction nodes (inferences and constructions), and enclosures (assumptions or subproof scopes). Expanding a box reveals its internal argument. Collapsing it retains an honest typed contract.
This is also related to string diagrams and proof nets. These traditions motivate compositional graphical reasoning but do not provide a universal semantics for all Lean proofs out of the box. There are also existing Lean-specific structural viewers: Lean Atlas and an independent, similarly named ProofAtlas that studies Lean expression hypergraphs and verified structural measurements. This project is not affiliated with that one; merely drawing a Lean graph is not a novelty claim. Our open question is whether exact graphs can support faithful, recursively expandable mathematical explanations.
The recursive tree is a way of reading a graph
A tree is a natural navigational instrument: a theorem has branches, each branch has its own supporting arguments, and a small lemma can itself become a new tree when opened.
Yet the actual dependencies need not form a simple tree. A lemma may be reused in several places; several independent premises may be needed jointly; bound variables refer to an enclosing scope; a proof by cases joins arguments made under different hypotheses. Forcing all these into a tree either duplicates information or silently removes it.
Our working model is therefore:
A typed dependency graph, organized into a recursive tree of explanatory modules.
Each module has a boundary: the assumptions and inputs it receives, the conclusion or construction it provides, and an underlying reference to exact formal evidence. A collapsed node is allowed to hide its interior. It is not allowed to delete necessary premises.
A proof by contradiction illustrates this boundary requirement. To establish $\neg A$, we introduce an assumption $A$ inside a scoped enclosure, derive False within that scope, and discharge the assumption. If we instead want to infer $A$ from $\neg\neg A$, we need an additional principle such as classical double-negation elimination (or a suitable decidability hypothesis). The graphical junction must show this change of scope, not depict an unexplained collision between two lines.
Induction has a different appearance: a finite box contains a base case, a step, and the legitimate recursor. An apparent loop in the drawing must never be mistaken for circular reasoning.
The first measured experiment
The benchmark is CrossingData.crossing, a counting lemma in a Lean formalization associated with a sub-Riemannian problem on $\mathrm{SE}(2)$. The underlying mathematical claim concerns a phase line intersecting a two-branch zero curve exactly once on an appropriate interval.
The existing exporter processed the elaborated theorem statement and proof term. The resulting CoreGIR expression-occurrence structure was transformed into a graph with explicit binder and declaration references. Seven local integrity tests passed, and a GitHub Actions run regenerated the export and viewer from Lean.
| Directly measured quantity | Value |
|---|---|
| Expression occurrences (type and value combined) | 7,288 |
| Structural child edges | 7,286 |
| Bound-variable-to-binder reference links | 431 |
| Constant-use occurrences | 2,892 |
| Distinct directly referenced constants | 42 |
| Maximum expression depth (edges) | 49 |
We also computed 665 distinct structural subtree fingerprints across the 7,288 occurrences. This is a preliminary syntactic statistic, based on constructor, payload and ordered child fingerprints. It does not show that 91% of the mathematical argument is redundant, that the associated proofs are equivalent, or that repeated subtrees may be identified across different binder contexts.
The public interactive atlas offers whole-proof geometry, a declaration-use constellation, recursive zoom and an editorial explanation. It ships only the anonymized structural projection: not the private Lean certificate text.
The mathematical idea we want the compiler to find
For this theorem, the source exposes two named lemmas, exists_branch and unique_branch. Together they support the final exactly-one result:
The existence result uses intermediate-value reasoning over phase intervals. The uniqueness result uses strict monotonicity within branches and the fact that apparent double descriptions at glued endpoints represent the same parameter. The proof is not justified by a winding-number slogan alone: a degree-one map need not be one-to-one.
For now, the diagram of this idea is an interpretation anchored to named formal results. The initial export references those two lemmas but does not contain their full internal proofs. Automatically recovering the concept map from transitive formal dependencies is the next challenge.
Research questions and failure criteria
We will measure progress against three questions—not declare them solved in advance.
H1 · Global structure. Is there stable, nontrivial organization in a full proof graph that survives reasonable choices of graph projection and layout? The claim fails if all apparent clusters are arbitrary layout effects or elaboration noise.
H2 · Faithful compression. Can a compiler collapse repeated or low-level proof structure into usable modules while preserving a typed interface and a complete path back to Lean? The claim fails if compression hides an indispensable assumption, introduces an unsupported inference, or breaks provenance.
H3 · Mathematical understanding. Does the multiscale explanation help a reader identify why a theorem is true more reliably than browsing the raw proof term? We need actual reader tasks and comparisons; appealing diagrams alone are not evidence.
The experimental sequence is: complete the transitive local dependency graph, build well-scoped recursive modules, test direct reasoning / contradiction / induction, then evaluate whether readers can locate the core mechanism of the SE(2) crossing argument.
Current verdict
Established: a real Lean proof can be converted into a complete expression-occurrence graph, audited numerically, and explored interactively in the browser. The first sample contains 7,288 nodes and connects syntax with direct declaration references.
Not established: that the graph geometry identifies the important mathematical ideas; that structural repetition is proof redundancy; that arbitrary Lean terms have concise, automatically discovered graphical explanations; or that such explanations measurably improve comprehension.
The distinction is the research program. We are trying to move from a correct map of a formal object toward a correct and illuminating map of its reasoning.
References and nearby work
- Lean 4: Expressions and Theorem Proving in Lean — the underlying term language and proof typing.
- Paperproof — visualizing Lean goals, contexts and proof development.
- Independent ProofAtlas — Lean-based proof hypergraphs and structural metrics; a separate project with a closely related name and research questions.
- Lean Atlas — declaration dependency exploration.
- Peter Selinger, A Survey of Graphical Languages for Monoidal Categories — formal compositional diagram syntax.
- Proof-net research — removing sequential bureaucracy in particular logical systems, not all dependent type theory.
- The interactive benchmark — the current measured structural visualization and its public-data limitations.