Reference

How to read Definograph’s views, what its checking evidence means, and the labels the views use.

Labels in bold are Definograph’s own. For source and setup information, see Try it yourself.

Recorded views on this site

A figure marked Recorded Definograph output is a saved copy of what Definograph drew for the Lean source printed with it. The copy is Definograph’s own HTML and SVG, so its text stays text and it scales without blurring. Every figure on this site is such a copy, whole or excerpt: the site publishes no screenshots or other pixel images of the app window.

This site runs no Lean and does not check any input. Controls in a recording do nothing; in the app they select objects or steps.

This page describes Definograph at its revision of 2 October 2026; Setup says what the current source changes.

Recorded Definograph excerpt marks a copy of only part of a panel. The top and bottom edges of its frame are dashed. A dashed line inside it marks any place where part of the panel between the parts shown is left out.

The source beside a figure is exactly what Definograph read: a complete Lean file, or a statement typed into the Lean expression field of Definograph’s Lean source panel. That field accepts a single statement term and has Lean read it with Definograph’s fixed imports.

The rest of a figure’s label gives its dates and says where its data came from. Figure labels and drawing details, near the end of this page, explains each part and lists the few things this site changes when it draws a recording.

How to read the views

Every view is a diagram of a statement’s structure. None is a proof. For a statement term, Definograph has Lean elaborate the term as a proposition (resolve its notation and fill in every type and implicit argument), then check the result with Lean’s kernel. That shows the statement is well formed, not that it is true.

Definograph works from this elaborated statement, not from its printed text or from theorem names. Objects keep their identity by where they were introduced, so two variables that print the same name stay distinct. Parts Definograph cannot interpret stay visible as typed or logical structure.

Definograph opens a statement with its Visual sequence. Under Explore a sample, the Choices, Relationships and Structure views appear as tabs, with numerical views such as Condition for some statements. The Mathematical notation button shows the statement typeset. In the app each view sits in a numbered card with a title, such as “Choices and dependencies”. The recorded figures on this site show the view without its card, on the card’s white background.

Choices

The Choices view, tagged “Scope and dependency”, lists what the statement introduces as numbered steps in reading order. Each step names its role: Arbitrary choice for a universal binder (∀, “a value from the full domain”), Candidate witness for an existential one (∃, “a candidate chosen at this stage”), and Assumption, Function input or Local definition where those occur.

Read it top to bottom. Under a candidate witness, May depend on lists the earlier choices in its scope that the witness may use. A candidate witness with no earlier choice in its scope says “Chosen without earlier values. Later choices cannot change this witness.”

What it leaves out: the condition the choices must satisfy, which you read in the source. A candidate witness is not a found witness: “Its existence remains an obligation.” A displayed sample of an arbitrary choice is one value, never every value. Choices in separate logical branches are not combined.

Relationships

The Relationships view, tagged “Symbolic view”, shows each relation Definograph recognizes as a card. A card gives the relation as written, its kind (for example Membership, Set inclusion, Equality, Comparison or Function application) and the objects that fill its roles, such as element and set, subset and superset, or function, input and output. It also notes when the relation sits under an assumption.

Read one card at a time, then follow an object that appears on several cards: it is the same mathematical object wherever it appears.

What it leaves out: “These are diagrams of mathematical roles. Relative position and distance carry no geometric meaning.” A relation drawn inside an assumption, a negation or an alternative is not a claim that the relation holds. The view shows at most eight relations and says so when there are more.

Structure

The Structure view, tagged “Structural view”, draws the objects of a statement in one column and its relations in another, with a connector from each relation to each object it uses. Select an object to highlight its connectors and trace it through every condition that mentions it.

What it leaves out: which relations are assumed and which are required. Position, distance and the curvature of connectors carry no meaning. Definitions Definograph does not interpret are not expanded. Some objects are not written in the statement, such as a, the name Lean gives an unnamed hypothesis, and some appear under Lean’s internal names, such as HasSubset.Subset(A, B) for A ⊆ B. Large statements are cut to a display limit, which the view states.

Visual sequence

Definograph’s first view of a statement moves through it one step at a time, with Previous, Next and a step selector. A Whole statement outline stays beside the steps, and the full visual statement is available below them. Each step introduces objects, follows a function application, compares two expressions or focuses on a logical condition. It names its role: parameter, arbitrary choice, requested witness, assumption, required conclusion, alternative or negated condition.

What it leaves out: a step that compares two expressions does not certify that they are equal. Alternatives are not accumulated as facts, and a negated condition stays under its negation.

Specialized figures

For some recognized vocabulary, the reading adds a figure. Definograph recognizes the forms it supports, not every way Lean can express the same idea; other expressions stay as typed or logical structure. All of these figures are schematic.

Set expressions

For up to three atomic sets, the figure divides the ambient type into membership regions: in or out of each set. A subset condition hatches the regions that must be empty. An equality hatches the regions where the two sides differ. A membership condition highlights where the element may lie, without choosing one region.

What it leaves out: “Regions encode membership combinations, not elements or sizes. Drawing a region does not assert that it contains an element.” With more than three sets Definograph lists construction steps instead.

Graphs and colorings

For Mathlib’s simple graphs, the figure shows what a condition requires of an edge. For a proper coloring: “For any adjacent endpoint pair, a proper coloring assigns unequal labels.” For a graph homomorphism, every edge is sent to an edge. For G.Colorable n, the palette is the set of labels available.

What it leaves out: “Endpoint slots stand for arbitrary inputs to the rule. They do not instantiate vertices, assert that an edge exists, or determine the graph’s size or shape.” The palette shows available labels, not a coloring; “a coloring may use fewer labels.”

Metric regions

For open balls, closed balls and spheres, the figure shows the distance condition, whether the boundary is included, what happens when the radius is zero or negative, and any local assumption such as 0 < ε. Where the metric and dimension are supported and values are chosen, Definograph can draw a sampled region, an adjustable coordinate slice, or a distance profile of one point.

What it leaves out: symbolic positions choose no coordinates, and named points may coincide. Numerical samples and coordinate slices are illustrations under the chosen values, not the statement. A slice keeps its ambient dimension; points off the slice are not projected onto it. The distance profile plots the absolute coordinate displacements of one point; its bars discard sign and are not the shape of the region.

Maps inverse on a region

For Mathlib’s PartialEquiv and OpenPartialHomeomorph, the figure shows two carriers, a source region and a target region, the forward and inverse maps, and the two round trips that return to their starting point on those regions.

What it leaves out: the carriers are abstract containers without geometry or coordinates. “Region frames indicate containment, not shape, size, dimension, connectedness, or a proper subset.” No inverse law is asserted outside the designated regions.

Structure and checking evidence in the editor

In VS Code, Definograph: Visualize Selection reads a selected expression in a trusted Lean project. Source data keeps the selected expression, its local declarations and every recorded checking outcome. Structure shows the term, its inferred type and its complete context as constructors with their ordered parts, binder scopes and references to declarations. Explicit actions expose one definition, check a chosen part, inspect a type or read one layer of logical structure. Each keeps its own recorded outcomes.

What it leaves out: reading a term’s structure back does not establish its typing. A refused or unavailable operation is a limit of Definograph’s coverage, not a sign that the Lean is invalid. The sections below explain the evidence these panels record.

Four kinds of information

Kinds of information
Kind	What it contributes
Lean checking	A typing or conversion outcome for one submitted declaration in one environment. Read its dependencies and any unavailable audit.
Semantic interpretation	A supported reading of the extracted structure, such as quantifier order or an audited mathematical relation. Unknown expressions keep their boundaries.
Schematic visualization	A presentation of that reading. Placement on the page adds no coordinates, nonempty regions or other mathematical assumptions.
Numerical sampling	Particular evaluated cases, where supported. Samples do not prove a universal statement or automatically supply an existential proof.

A claim about one kind is not automatically a claim about all four. In particular, kernel acceptance does not certify the rendered diagram or show that its explanation is useful to you.

Checking evidence

Several different facts can come with a reading. Keep them apart:

Accepted typing: Lean’s kernel accepted one submitted declaration in the captured environment. For a proposition, that shows the statement is well formed. It does not show the statement is true, unless the declaration supplies a proof, and then only relative to the environment and its axioms.
Formation: evidence that an expression is a proposition, a type, a sort or an ordinary term. Forming a proposition does not prove it.
Axiom audit: the global axioms a checked declaration depends on, or the reason the audit is unavailable. An empty audit for one check says nothing about another.
Direct sorry: Definograph refuses a statement term that contains sorry, and the editor marks placeholder-containing terms unsupported before checking.
Transitive sorryAx: a declaration can depend on an unfinished proof elsewhere. Only the axiom audit shows this dependency.

Read the context, the recorded outcomes and the axioms together. Saved records are unverified and carry no current authority.

RecordedAxiom.leanDownload

theorem claimed : 2 + 2 = 5 := sorry
example : 2 + 2 = 5 := claimed

Read the placeholder dependency

This file deliberately leaves a proof unfinished with sorry. Lean accepts the declarations and warns that a declaration uses sorry. The placeholder adds a dependency on sorryAx. The second declaration refers to claimed, so it keeps that dependency.

Accepted typing here is relative to an environment that contains the placeholder dependency. Neither declaration independently establishes the false equation 2 + 2 = 5. Read the typing outcome together with its axiom audit; an empty audit for a different formation check cannot replace it.

Context and identity

Names in scope lists the names that can be used at that point of the source. A context can contain user parameters, local definitions, recorded auxiliary declarations and binders entered during inspection, each with a different role. Listing an entry does not assert that the selected term uses it.

Names alone do not establish identity: two objects with the same displayed name need not be the same object. Read the context position, the expression’s constructor path and the relation through which it was reached. Fields and laws belong to their recorded owner and stay available within that owner’s scope.

Relations between expressions

Reading relations
Relation	Reading	Boundary
Containment	An expression occurs at a particular constructor position inside another expression.	Entering it does not construct a proof of it or specialize an enclosing proof.
Type-of	The second expression is the inferred type of the first at the captured universe levels.	It is not interchangeable with an unchecked source annotation.
Projection	A field is taken from a particular recorded owner.	Matching field names do not identify different owners.
Conversion	A requested definition-head or projection conversion has its own recorded outcome.	It does not authorize arbitrary simplification.
Formation	Evidence supports reading the occurrence as a proposition, type, sort, or ordinary term, or leaves that reading unestablished or conflicting.	Forming a proposition does not prove it.
Supply	When a term’s typing is accepted and its type is established as a proposition, the term can be read as supplying a proof of it, relative to the entries, frames and axioms the reading lists.	Read the complete context and typing audit; neither axiom independence nor a separate proof of a contained expression follows.

One physical check can serve more than one role; counting it twice gives no independent confirmation. Occurrence, relation, step and outcome numbers refer to different things. The relations guide (a Markdown file) gives the full reading and navigation boundaries.

An attempt records a bounded sequence of requested inspections and their outcomes. Step reading, Ordered provenance and Supply reading describe the selected step or the prefix through it. Attempt outcomes keeps the whole attempt, including checks outside that prefix.

Section navigation and its return links move reading focus within the displayed attempt and step. They do not change the selected attempt, open disclosures or run Lean. Explicit inspection actions make fresh captures; selecting retained data or changing its presentation does not.

Inspect type makes the inferred type the next term. Read logical structure of this term (one layer) inspects the displayed term. To inspect the logical structure of its inferred type, inspect the type first. Operations are bounded and can be refused or unavailable; those states must remain visible.

A law belongs to its owner

RotorLaw.leanDownload

structure Rotor where
  Carrier : Type
  turn : Carrier → Carrier
  fixed : ∀ x, turn x = x
example (owner : Rotor) (unused : Nat) : Rotor := owner

The example takes owner : Rotor as a parameter. Its fixed field already supplies a law about that owner’s turn. The example does not construct a Rotor or independently establish its law.

The inspection route catalogs the fields, projects fixed, inspects its type, reads the universal layer and enters its body. A field catalog by itself is not a typing check. Inspecting the equality inside the law does not produce a separately specialized proof of that equality.

Keep the full context, including unused, when reading the conditions. The presence of unused does not assert that the proof depends on it. Recorded auxiliary entries also keep their own kind.

The first guided view of the selected structure value can refuse to give a reading. The saved source and the route of checked occurrences are separate from that view’s answer. The source’s unused-variable warning is a diagnostic, not a rejected kernel outcome.

Recorded data and live editor context

Saved records have an unverified origin. Recorded outcomes do not establish that a file describes the current buffer, engine or imported environment. Format validation and internal consistency do not authenticate the recorded computation.

This site offers no live checking of your input.

In the editor, a reading belongs to the file and the selection it was made from: it stops being valid when you edit the file or change the selection. The editor has Lean read the whole trusted file again, as it stands in the editor and including commands outside the selected range, against the dependencies that are already built. Lean commands and elaborators can execute code. A separate process and resource bounds do not make that execution a security sandbox.

Setup and support

Running Definograph yourself currently means assembling it from source; Try it yourself explains what is published. A matching public distribution with qualified installation, upgrade, rollback and uninstall paths is not yet established. A public clone, or the editor extension package alone, need not reproduce the build described here.

The Setup page lists the requirements and the configurations that have been checked. For local assembly, the local setup guide gives the command sequence and qualifications. You can read the lessons and recorded figures without any of this setup.

Generality and formal foundations

The formal foundations already prove general results about specified encodings of Lean expressions and local source records: decoding an encoding recovers the expression’s structure, and the encoded forms can be printed as text and read back exactly. A readback result states what can be recovered by decoding an encoding. Two examples in the foundation dependency retained by this build are:

ExprReferenceGraph.roundTrip_eq: decoding the reference-graph encoding of a Lean expression recovers that expression after eraseMetadata. This is an explicit normalization boundary; the theorem does not assert preservation of expression metadata or original source text.
FoundationIntegration.encodeView_readback: when encoding into the scoped view succeeds, decoding recovers the expression after the same metadata erasure. Its coverage result applies only when the declared admission conditions hold.

At the current source, ExprReferenceGraph.roundTrip_eq depends on no axiom and FoundationIntegration.encodeView_readback depends on propext, Lean's propositional extensionality axiom. These are formal results about the named representations and decoders. Separately, browser structural views implement independent reconstruction checks for their supported inputs. Neither fact establishes a Lean proof about the complete browser renderer, authenticates an imported record, or proves a proposition merely because it can be represented.

The goal remains a formally proved general visualization method for any valid Lean mathematical statement. The current application provides bounded structural inspection and selected guided readings; a universal guarantee connecting valid inputs to the rendered interactive view remains unproved. Extending the foundations across the complete application, including its context and scope handling, semantic readings, and renderer, remains open work. Interpreting unfamiliar mathematics, selecting useful abstractions, and demonstrating improvements in human understanding are further research questions.

What Definograph supports today can still be useful. Judge each reading by what it keeps: the expression, its context, any transformation, the evidence and the stated limits.

Figure labels and drawing details

The label above a figure can say:

A Lean version and one date only: An older figure. The label gives the Lean version and the date the figure was recorded. That date does not by itself say when Lean ran.
Rendered, with a date: The figure was drawn again from saved results, without rerunning Lean. The drawing may come from a newer version of Definograph; the captured results and the source are unchanged. It is not a fresh Lean check, and it gives the saved data no current authority.
Native capture, with a date or a range of dates, or Native capture date unavailable: When the saved results were first captured, kept apart from the date of the new drawing, or a statement that this date is not available.
Dates in UTC: The dates in the label use UTC.
Saved input: Lean 4.28.0: The Lean version belongs to the saved input.
From a saved history, or from saved results: From a saved history means the figure was drawn from a saved history of inspection steps in the editor. Other saved results are labelled from saved results. A label without “from a saved history” does not mean the figure came from a live editor session. A panel drawn from saved data outside Visual Studio Code says so in its label, and its caption describes it. Where a figure says where saved data came from, it keeps Definograph’s own cautions, such as “This saved history has an unverified origin”.
Adapts to page theme, Light theme or Dark theme: A figure that says Adapts to page theme was recorded with styles for both a light and a dark page. This site has a light theme only, so here it always uses its light styles. Light theme or Dark theme gives the recorded theme of a figure with one fixed theme.

The site changes only these details of how a recorded figure is drawn:

The outline that marks keyboard focus is blue.
A step selector shows its whole entry instead of cutting it off.
The “Whole statement” outline and the Structure view’s map are shown in full instead of in a scrolling box.
An outline or a coverage report shown on its own has no rule above it.
A reading step recorded without the outline is drawn across the space the app keeps for the outline.
In an excerpt from the editor’s history, a panel whose heading the excerpt leaves out is drawn without its outline. The outline around the text that is shown stays.
The round-trip diagram of Lesson 7, which the app shows in a scrolling box, takes the width of its frame. On a wide screen it is drawn about 3% smaller, and on paper smaller still, so that the whole route shows.
On wide screens, figures that still fit are drawn 1.125 times as large as in the app. Figures with typeset mathematical labels are the exception: they keep the app’s size, so that the labels stay in place.

On a narrow screen a wide diagram keeps its own size and scrolls sideways inside its frame, so its labels stay readable. On a wide screen the frames of the widest diagrams extend past the text column, and the “Whole statement” outline, a narrow column in the app, has a frame of its own width. On paper nothing can scroll, so a figure wider than the page is printed a little smaller to fit. Apart from that round-trip diagram, figures with typeset mathematical labels are not made smaller, and the widest of them runs past the edge of an A4 page.

Typeset mathematical labels keep accessible MathML and use bundled local fonts. The recorded figures are static HTML containing SVG and mathematical HTML; they need no client-side math renderer and are not portable standalone SVG files.

Glossary

Terms used on this site and labels that appear in Definograph, in alphabetical order.

Arbitrary choice: Marked ∀. A variable for which the rest of the statement must hold whatever value it takes. A sample shows one value, never every value.
Assumption: The hypothesis of an implication, marked ⇒ in the Choices view. What follows it is required only when the hypothesis holds. An assumption that has no name in the statement is shown with the name Lean gives it, a; that a is a name, not a kind badge.
Attempt: One run of a history’s steps in the editor. Acting from an earlier step starts a new attempt and keeps the old one. Each attempt has a short random identifier.
Auxiliary entry: A context entry that Lean adds itself while it checks a declaration, such as _example for an example, or a theorem’s own name. Its recorded kind is auxDecl. It is not an assumption.
Axiom: A statement that Lean accepts without proof, such as propext, or sorryAx, which stands for a missing proof.
Axiom audit: The axioms that a checked declaration depends on, as Lean recorded them, or the reason they are unavailable. An empty audit for one check says nothing about another.
Binder: The place where a statement introduces a variable, such as ∀ x : ℝ.
Candidate witness: Marked ∃. A variable that the statement asks to exist. The view names it but does not supply a value.
Carrier: The whole type that a map or a region lives in, as opposed to a region inside it.
Check: One declaration that Definograph submits to Lean’s kernel. Its outcome is accepted, rejected or unknown.
Choices: Under Explore a sample, the view that lists the choices and assumptions in the order the statement makes them, and which earlier choices each one may use. It leaves out the conditions the choices must satisfy.
Choices and dependencies: In the app window, the title of the card that holds the Choices view.
Condition: A numerical view under Explore a sample, for a comparison such as x < y: it varies one variable while the other choices stay fixed. Also a stage label: a step that reads a relation such as membership or inclusion, assumed or required.
Conditional on the premise: A tag on a part of the statement that comes after the premise of an implication: it applies only when the premise holds.
Connected objects: In the app window, the title of the card that holds the Relationships view.
Context and component: The two halves of most checks: the declarations around the selection, and the selection itself in that context.
Context entry: A declaration available at the selection, such as a variable or a hypothesis. The editor shows each one with its recorded kind, such as default or auxDecl. A variable that the enclosing declaration does not take, or may not take, is listed under the guided reading’s title instead of drawn. An instance written without a name, such as [Inhabited β], is shown with the name Lean gives it, inst.
Continuation: A history built by acting on a selection step by step. “Current continuation” names the attempt shown.
Diagnostic: A warning or error that Lean reported while reading the file, listed under Lean diagnostics. It is separate from any check outcome.
Earlier choices in this scope: The choices made before this one within the same scope.
Elaborated statement: The statement after Lean has resolved its notation and filled in what the source leaves implicit, such as types and hidden arguments. Definograph reads this, not the printed text.
Excerpt: A recorded figure that shows only part of a panel.
Explore a sample: The group of tabs that holds the statement’s other views: Choices, Relationships and Structure, and for some statements numerical views such as Condition or Geometry. A numerical view shows one sample of values, never the statement.
Formation: Whether Definograph read an expression as a proposition, a type, a sort or an ordinary term. It reads this only from logical and type inspections, so “not established” can appear for an expression that is in fact a proposition.
Frame: In a supply reading, a relation passed on the way from the selection to the term, such as taking a field of a structure (a projection).
Function input: An input binder shown in an expression reading, including a lambda or a dependent-function binder. In a component reading, this label alone does not establish the binder’s logical role.
History: The steps you take from a selection in the editor, each one recorded with its checks.
Identity thread: In the Visual sequence, a dashed line that joins the places where one selected object appears. Its route means nothing.
Interpretation coverage: In the Inspect panel, the section that counts the parts of a statement Definograph could interpret, and names the definitions it left folded.
Kernel: The part of Lean that has the final say on whether a term has a given type.
Kind badge: The small mark before an object’s name that gives its kind: a for a number, { } for a set, ↦ for a function, T for a type, ⋯ for an expression built from other objects and x for a variable of any other type. Less often it is • for a point, # for a literal or s for a named constant.
Local definition: A name given a value inside the statement, with the value it stands for.
matched, new: Marks on the steps of a history: matched means that the step was computed again with the same result as before; new marks the step just requested.
Mathematical notation: The button that shows the statement typeset.
May depend on: The earlier choices a candidate witness is allowed to use. It permits dependence; it does not require it.
Occurrence: An expression that a history reached, numbered in order. Occurrence 1 is usually the selection.
Owner: The object whose fields a panel lists. Every field belongs to it, as e.source belongs to e.
Prefix: The part of a history up to the selected step.
Premise of an implication: A tag on a part of the statement that lies in the premise of an implication: it is assumed there, not claimed. Numerical views call it Assumption of an implication.
Receipt: A recorded check outcome that a reading rests on. One receipt can serve two roles, for example typing and formation.
Recorded context entry: In the Choices view, an entry that Lean added to the context itself, such as an auxiliary entry, shown with its own kind. It is not an assumption of the statement.
Recorded figure: A saved copy of Definograph’s output on this site. Nothing in it is computed again, and its buttons do nothing.
Relationships: Under Explore a sample, the view with one card per relation: each object in its role, and tags that give the relation’s place in the logic of the statement.
Saved record: A history or snapshot written to a file. Definograph marks its origin as unverified, and nothing in it is checked again.
Scope and dependency: The tag on the Choices view: it shows scope and permitted dependence, not values.
Source data: In the editor, the exact records of a selection, in four tabs: Original data, Checker input, Expected type and Check outcomes. In the browser app, the Source data link opens a page that inspects such data from a saved file.
Stage label: The small capitals above a step’s title in the Visual sequence, which say what kind of step it is. Objects and choices introduces variables. Logical structure sets out implications and other connectives. Condition reads a relation such as membership or inclusion, assumed or required. Compare reads an equation or inequality between two expressions. Construction reads how an object is built, for example by applying a function. Inside the expression reads a part of a larger expression. Recorded context shows an entry that Lean recorded in the context, such as _example.
Statement structure: In the app window, the title of the card that holds the Structure view.
Structural view: A view of expression structure only, with no geometric or numerical meaning.
Structure: Under Explore a sample, the view that shows the displayed objects and relations in one overview, with a line for each role. The Structure tab of the Lean source panel is different: it lists the statement’s logical parts.
Structure only, folded: A part that Definograph shows as a name and its arguments, without interpreting its meaning. Interpretation coverage counts such parts as structure only, and lists the definitions whose meaning is still folded.
Supply reading: A reading that a term supplies a proof of a statement, relative to the listed entries, frames and axioms.
Symbolic region · no coordinates assumed: A metric region drawn by its role (center, radius, region) without choosing coordinates.
Symbolic relation: A relation Definograph recognizes as a predicate applied to its arguments, without further interpretation.
Symbolic view: The tag on the Relationships view when Definograph recognizes the relations it shows, such as membership or set inclusion. The cards show roles, with no geometric meaning.
Under N assumptions: A tag that counts the assumptions in force at that point. In the Choices view, an assumption’s own step counts that assumption too. Numerical views say “Under 1 local assumption”.
Visual sequence: Definograph’s step-by-step reading of a statement, with the whole statement alongside, and the first thing it shows.
Well formed: Accepted by Lean as a proposition. It says nothing about whether the statement is true.
Whole statement: The outline beside the visual sequence: every choice, assumption and requirement in its logical place, with the current step highlighted.