Reading mathematics with Definograph
Definograph reads a mathematical statement written in Lean and draws what it says: which objects it introduces, which choices may depend on which, how the objects are related, and which parts are only assumed. This tutorial uses those views to read a statement’s assumptions, conclusion and dependencies.
Each lesson shows what Definograph draws for a statement, how to read the drawing, and what the drawing does not tell you. Exercises follow. Each has an answer and most have a hint; try the question before opening either.
Where to start
Start with Lesson 1. It has the first figures, and each lesson explains the Lean notation it uses.
The worked example, Reading the Lebesgue-number lemma, reads a theorem from Mathlib in the same way: its hypotheses, its quantified choices and its whole-ball conclusion. That page has no figures. If you are new to Lean, read its short notation guide first.
Before you begin
You should be comfortable with ∀, ∃, sets and functions. You do not need to know Lean: each lesson explains the Lean notation and the other terms it uses where they first appear. The Reference collects the terms in a glossary.
The figures are recorded output of Definograph, with Lean 4.28.0. Each one says that it is recorded, gives the date, and shows the exact source it was made from. A recorded figure is a copy: its buttons do nothing and nothing in it is recomputed. This website does not run Lean or Definograph.
To try the statements yourself, you need Definograph running on your own computer. Try it yourself, in Setup, says what that takes and what is available today. Lessons 1–4 use statements from Definograph's own Statement menu, which it checks against its pinned copy of Mathlib, Lean's mathematics library. Lessons 5–7 use the Visual Studio Code extension with small Lean files that you can download; those files need only Lean 4.28.0.
Where the views appear
Definograph shows a statement in several ways. The lessons use the names on its buttons and tabs:
| Name in Definograph | What it shows | Lesson |
|---|---|---|
| Visual sequence | The statement one step at a time, with the whole statement alongside. This is what Definograph shows first. | 2 |
| Choices | The quantified choices in order, and which earlier choices each may use. It leaves out the conditions. | 1 |
| Relationships | Each relation, the objects it connects and the role of each object. | 2 |
| Structure | The displayed objects and relations in one overview, with lines between them. | 2 |
| Specialized figures | Set regions, graph colorings, metric regions and maps that are inverse on regions, inside the Visual sequence. | 3 |
| Inspect | Definitions opened for reading, the objects, and what Definograph could not interpret. | 4 |
| Source data | In the editor: the selected expression, its context and the checks Lean ran. | 5, 6 |
Explore a sample holds the other representations of the statement as tabs: Choices, Relationships and Structure, and, for some statements, numerical ones such as Condition or Geometry. The Mathematical notation button shows the statement in ordinary mathematical notation. The Lean source panel also has a tab called Structure. That tab is a different thing: it lists the statement's logical parts.
Lessons
| Lesson | What you do | What you should be able to explain |
|---|---|---|
| 1. The order of choices | Compare two statements that differ only in the order of their quantifiers. | Which choices may depend on which, and why the view does not decide truth. |
| 2. Objects and relations | Trace objects through the relations of a statement. | Which relations are assumed, which are required, and what connects them. |
| 3. Specialized figures | Read set regions, graph colorings, metric regions and restricted inverses. | What each figure adds, and what it states it does not claim. |
| 4. Inside definitions and structures | Open a definition and read a structure's fields and laws. | What a name hides, and what opening it shows. |
| 5. Inspecting a selection in the editor | Select a statement in Visual Studio Code, find the same views, and check a part of it. | Where Definograph keeps what Lean checked, and how to read it one layer at a time. |
| 6. Checking evidence | Compare a well-formed statement, a proof from a hypothesis and an unfinished proof. | What Lean checked, and what it did not. |
| 7. An unfamiliar structure | Read a new structure, then compare your reading with Definograph's figures. | What the figures show about a definition Definograph has never seen. |
Three questions to keep asking
- What does the statement say? Its choices, its assumptions and what it requires.
- What does this view show, and what does it leave out? Every view leaves something out; each lesson says what.
- What has been checked? Lean checked that the statement is well formed. That is not a proof, and a drawing of a statement is not evidence that it is true.