Definograph

Definograph

Definograph draws the structure of a mathematical statement written in Lean: the order of its choices, which variables may depend on which, its assumptions and requirements, and the definitions behind them. It reads the statement as Lean has understood it, with notation resolved and every type filled in, not as printed text. It does not prove statements or say whether they are true. Definograph is a research prototype that runs on your own computer. The figures on this site are its recorded output. The site runs no Lean, so you can read everything here without installing anything.

Start reading: Lesson 1, the order of choices →

Below are two views of two statements. Choices reads ∀ x : ℝ, ∃ y : ℝ, x < y from the top: x is chosen first, and y may depend on it. Relationships reads A ⊆ B → x ∈ A → x ∈ B one relation at a time.

Recorded Definograph output · Lean 4.28.0 ·

Lean statement, as entered in Definograph

∀ x : ℝ, ∃ y : ℝ, x < y

A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.

Scope and dependency
∀ a value from the full domain∃ a candidate chosen at this stage
  1. 1
    Arbitrary choicex : ℝ

    An arbitrary element of this type. A displayed sample represents one choice, never every element.

  2. 2
    Candidate witnessy : ℝ

    Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.

    May depend on
    x

Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.

Definograph’s Choices view, tagged “Scope and dependency”. x is chosen first; y comes second, and its May depend on list names x. The small a before x marks its kind, a number. The view leaves out the condition x < y.

Recorded Definograph output · Rendered · from saved results · Adapts to page theme · Native capture date unavailable · Dates in UTC · Saved input: Lean 4.28.0 · Lean was not rerun.

Lean statement, as entered in Definograph

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

Read each relation through its objects and their roles. Repeated objects stay linked across views.

Symbolic view
01
Set inclusion

is a subset of

Premise of an implication
subsetASet ℝsupersetBSet ℝ
02
Membership

belongs to

Conditional on the premisePremise of an implicationUnder 1 assumption
elementxℝsetASet ℝ
03
Membership

belongs to

Conditional on the premiseUnder 2 assumptions
elementxℝsetBSet ℝ

These are diagrams of mathematical roles. Relative position and distance carry no geometric meaning.

Definograph’s Relationships view, tagged “Symbolic view”: one card per relation, with each object in its role and tags that say where the relation sits in the statement. A relation under an assumption is not claimed to hold.

Reading order

  1. Lesson 1: The order of choices: which choice may depend on which?
  2. Lesson 2: Objects and relations: which relations does an object take part in?
  3. Lesson 3: Specialized figures: what does a condition require?
  4. Lesson 4: Inside definitions and structures: what does a name hide?
  5. Lesson 5: Inspecting a selection in the editor: where does Definograph keep what Lean checked?
  6. Lesson 6: Checking evidence: what did Lean check, and what did it not?
  7. Lesson 7: An unfamiliar structure: what do the figures show about a definition Definograph has never seen?
  8. Reading the Lebesgue-number lemma: what does a theorem from Mathlib assume, choose and conclude? A worked example in words; it has no figures.

The Tutorial introduces the lessons and their exercises. Examples collects recorded views of real statements with their sources. Reference explains how to read each view and what checking evidence means. Setup says how to try Definograph yourself.

Status

Definograph is not a general mathematical visualizer. It runs beside Lean 4.28.0 on your own computer. Its source is in the Definograph GitHub repository. Try it yourself gives the build and setup requirements.

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. These results say what can be recovered from an encoding under its stated conditions. The Reference explains what they cover.

The goal is 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. Mathematics that Definograph does not interpret stays visible as typed or logical structure.