Live demo¶
These pages are the web reader of three example articles, built from the reports their certificates wrote. Each is a short paper in the usual style, with an introduction and references, and each renders from its LaTeX source with a marker at the start of every sentence. Select a marker to see what Lean checked for that sentence: its formal reading, its Lean statement, its definedness condition, the premises it rests on and the declaration that justifies it.
-
The certified note
A number and its reciprocal, the note of the tutorial: a short article with an introduction, remarks between the results and references. Every one of its 7 claims is derived in the text from what it cites, and the explanations around them are prose.
-
The draft with a false theorem
The same note at step 6 of the tutorial: the theorem says
f(x) > 2, Lean refutes it atx = 1, and the corollary that rests on it is not verified. -
Three means
The harmonic, geometric and arithmetic mean of two numbers: symbols defined inside a theorem, in a
where-clause and in apposition, and an equality case read as "if and only if". 16 claims, all verified.
The markers¶
| Marker | Status of the sentence |
|---|---|
| Derived from its citations: a proof step, or a result whose proof compiled, proved in Lean from exactly what it rests on | |
| Checked by a companion development: a result stated without a compiled proof, proved in Lean | |
| A definition, well defined | |
| Compiled, not yet verified: no proof yet, or it rests on a claim that is not verified | |
| False as stated: refuted in Lean | |
| Not compiled: an undefined symbol or a construction the grammar does not read | |
| Prose: it asserts nothing checked |
The summary at the top of each page counts the claims by status, and the legend filters the markers.
The files behind the pages¶
| Page | Folder | Files |
|---|---|---|
| The certified note | examples/Demo |
article · proofs · report · draft |
| The draft with a false theorem | tests/Refuted |
article · proofs · report |
| Three means | examples/Means |
article · proofs · report |
CI certifies all three on every push, so the reports cannot go stale. To build the reader of your own article, see step 8 of the tutorial.