Read the structure of a mathematical statement
Definograph is an experimental Lean-backed reader for exploring mathematical statements through their types, definitions, and logical context. It helps you follow which objects are introduced, how expressions depend on them, and what a recorded check establishes.
The same symbols can say different things
∀ x : Nat, ∃ y : Nat, y = x
∃ y : Nat, ∀ x : Nat, y = x
The first statement allows a choice of y for each x. The second requires one y to work for every x. Quantifier order changes the statement even though the symbols and final equality are the same.
∀ x : Nat — for every x
∃ y : Nat — there is a y
The choice of y may depend on x.
y = x
∃ y : Nat — there is one y
∀ x : Nat — for every x
The same y must work for every x.
y = x
These schematics illustrate the quantifier scopes. They are not output from the Definograph reader. The complete source examples form these propositions without supplying proofs.
The tutorial starts with this comparison. You can read it here without installing software or signing in.
What you can explore today
The local reader provides guided views of supported logical and mathematical structures. Its editor integration can retain a selected expression, its context, and recorded checking outcomes from a trusted Lean project. Explicit, bounded inspections can expose a definition head, inspect a direct record field, follow a contained expression, or read one layer of logical structure. Expressions that are not interpreted remain visible.
The public lessons explain these distinctions using complete Lean source examples. Reading this site does not run Lean on your input. Local editor use requires a matching engine, browser build, Lean environment, and extension controller; see setup and support.
The goal and the current boundary
The foundations already prove general structural and exact printable readback results for specified representations of Lean expressions and local source records. These results state what can be recovered from an encoding under its declared conditions. The reference explains what these results 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. General mathematical interpretation and useful visual explanation remain research problems.
A successful Lean check, a semantic reading, a schematic diagram, and a numerical sample provide different kinds of information. The reference explains how to keep them distinct.