Reading mathematics with Definograph
A mathematical statement tells you what objects are available, which choices may depend on earlier ones, and what must hold. A useful visual reading makes those relationships easier to follow. To interpret it well, you also need to distinguish the statement from a proof and understand what a recorded check establishes.
This tutorial develops those skills through a small set of complete Lean examples. You will compare two statements that differ only in quantifier order, construct and examine proofs, follow an inspection history, and read the laws of an unfamiliar mathematical structure.
By the end, you should be able to explain a displayed statement in ordinary language and trace the evidence behind that explanation.
Before you begin
You need familiarity with equality, functions, and natural numbers. No previous Lean experience is required; each piece of Lean syntax is introduced when it becomes useful. The optional final proof asks you to follow a short chain of equalities.
You can complete all reading exercises without installing software. Every exercise has a worked answer, and many also offer a separate hint. Try the question before opening either. The hints and solutions are part of the lesson; they do not run a checker or record your answers.
The downloadable examples were checked with Lean 4.28.0 and its standard library. They do not require mathlib. If you already have that toolchain, run a file with lean FileName.lean, replacing the filename with the downloaded file. Expected messages are explained beside the example. A file can contain a deliberate unfinished proof and still finish with a warning, so read the messages as well as the exit status.
Local Definograph activities assume an existing matching editor installation. The reader behavior described here is pinned to revision e10da0157aa477e1cf2382ddde65e32aa96f25f6. There is no live Lean session or saved-history player on these lesson pages. Installation and support details are in the reference.
The learning sequence
| Lesson | What you will do | What you should be able to explain |
|---|---|---|
| 1. Follow the scope | Compare two quantifier orders. | Why a witness may depend on an earlier variable. |
| 2. Form a proposition, supply a proof | Read and check a proof and a refutation. | Why accepting an expression of type Prop does not prove it. |
| 3. Follow an inspection | Distinguish presentation, inspection actions, and retained history. | Which expression and which checks belong to the selected reading. |
| 4. Keep a law with its owner | Read a structure's fields and use its law. | Why ownership, scope, and the type of each field matter. |
| 5. Read the checking evidence | Compare a complete proof with an unfinished one. | How context, outcomes, diagnostics, and axiom dependencies differ. |
| 6. Read an unfamiliar structure | Work through a new example before opening its explanation. | How to justify a reading without guessing meaning from names. |
The examples build on one another. Lessons 1–2 establish the mathematical and Lean distinctions; lessons 3–5 apply them to the reader; lesson 6 brings them together.
Keep three questions in view
As you work, ask:
- What is the expression? Read its quantifiers, inputs, and scope.
- How did we reach it? A contained part, a field, and an inferred type have different relationships to the starting expression.
- What evidence applies here? Look at the particular recorded check, its context, and its dependencies.
These questions are useful even when a picture is immediately persuasive. The picture helps you understand the reading; the expression and its evidence tell you what that reading is entitled to say.