Paperproof will inspect how the hypotheses and goals were changing throughout the Lean 4 proof, and display this history - making it equivalent to how we think of a mathematical proof on paper.
In the following tables, you can see what tactics such as apply, rw, or cases look like in Paperproof; and how Paperproof renders real proofs from well-known repos.
Common tactics
| Lean | Paperproof |
|---|---|
|
apply |
|
theorem apply (a b: ℝ) : a = b := by
apply le_antisymm |
|
|
have | |
theorem have (a b: ℝ)
(h1: a ≤ b) (h2: b ≤ a) : True := by
have hi := le_antisymm h1 h2 |
|
|
intro | |
theorem intro
: ∀ (N: ℕ), ∃ M, N + N = M := by
intro n |
|
|
rw | |
theorem rw (a b: ℕ)
(h1: a = b) : (10 * a = 666) := by
rw [h1] |
|
|
by_contra | |
theorem by_contra (m: ℕ)
: 2 ≤ m := by
by_contra h |
|
|
use | |
theorem use
: ∃ x: ℕ, x = 5 := by
use 42 |
|
|
induction | |
theorem induction (n: ℕ)
: Nat.mul 0 n = 0 := by
induction' n with k ih |
|
|
cases | |
theorem casesN (n: ℕ)
: Nat.mul 0 n = 0 := by
cases' n with m |
|
theorem casesAnd (A B C: Prop)
(h: A ∧ B) : C := by
cases' h with a b |
|
theorem casesOr (A B C: Prop)
(h: A ∨ B) : C := by
cases' h with a b |
|
inductive Random where
| hi: ℕ → String → Random
| hello: (2 + 2 = 4) → Random
| wow: Random
theorem casesRandom (C: Prop)
(h: Random) : C := by
cases' h with a b c |
|
Full-fledged proofs
|
Mathematics in Lean (Jeremy Avigad, Patrick Massot) |
|
|
|
Hitchhiker's Guide to Logical Verification |
|
-
Install the "Paperproof" vscode extension (link).
-
You're done!
Now, click on the paperproof icon (after you installed the Paperproof extension, it should appear in all
.leanfiles), this will open a Paperproof panel within vscode.
You can click on any theorem now (well, only on tactic-based proofs, those starting with
by) - you should see your proof tree rendered.
Paperproof lives entirely in the vscode extension, so updating it means updating the extension - which vscode does automatically. You can check for new updates with cmd+shift+p => "Extensions: Show Extension Updates".
If you worked with formal proofs before, you might find Paperproof most similar to proof trees/Gentzen trees. The resemblance is not spurious, we can easily mimic Semantic Tableaux and Natural Deduction trees with Paperproof. All of these interfaces show "the history of a proof" - the way hypotheses and nodes were changing throughout the proof.
Unlike Gentzen, we can make use of css and javascript - so there are many visual syntax sugars on top of what would be a formal proof tree:
- hypotheses aren't repeated when used multiple times,
- goals and hypotheses are visually differentiated,
- variable scopes are shown as darkening backgrounds,
- available hypotheses are indicated via node transparencies,
- and so on.
Below, you will see a table with the main features of Paperproof.
Paperproof walkthrough
| Lean | Paperproof |
|---|---|
|
Hypotheses are displayed as green nodes, goals are displayed as red nodes, tactics are displayed as transparent nodes with dashed borders. |
|
|
|
|
A proof should be read "towards the middle". So, hypotheses should be read from top to bottom; and goals should be read bottom up. |
|
|
|
|
To zoom in on a particular dark box, you can click on it. Hint: these boxes represent variable scopes. Don't overthink this however, we'll always highlight the available hypotheses as you're writing the proof, consider these boxes a visual hint that will eventually become second nature. |
|
|
|
Theoretical:
- Paperproof
♥️ Semantic Tableaux: link - Paperproof
♥️ Natural Deduction: link - Paperproof ⚔️ Lean's #explode: link
- Lean ⚔️ Coq ⚔️ Metamath ⚔️ Isabel proof trees: link
Practical:
- Can Paperproof render proof terms: link
- Paperproof's Architecture: link
- Anatomy of the InfoTree: link, link
Videos:
- a super quick 1-minute demo of Paperproof: youtube link
- our Lean Together presentation: youtube link
- a full Paperproof tutorial: youtube link
- a full Paperproof tutorial - More Features (LaTeX, Snapshots, and Single-Tactic Mode): youtube link
You're welcome to contribute to Paperproof, see the instructions in CONTRIBUTING.md.
