Paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Install / Use
/learn @Paper-Proof/PaperproofREADME
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.
apply
</td> </tr> <tr> <td>theorem apply (a b: ℝ) : a = b := by
apply le_antisymm
have
</td></tr> <td>theorem have (a b: ℝ)
(h1: a ≤ b) (h2: b ≤ a) : True := by
have hi := le_antisymm h1 h2
intro
</td></tr> <tr> <td>theorem intro
: ∀ (N: ℕ), ∃ M, N + N = M := by
intro n
rw
</td></tr> <tr> <td>theorem rw (a b: ℕ)
(h1: a = b) : (10 * a = 666) := by
rw [h1]
by_contra
</td></tr> <tr> <td>theorem by_contra (m: ℕ)
: 2 ≤ m := by
by_contra h
use
</td></tr> <tr> <td>theorem use
: ∃ x: ℕ, x = 5 := by
use 42
induction
</td></tr> <tr> <td>theorem induction (n: ℕ)
: Nat.mul 0 n = 0 := by
induction' n with k ih
cases
</td></tr> <tr> <td>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
Mathematics in Lean (Jeremy Avigad, Patrick Massot) <br/>(mathematics_in_lean/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean:155)
</td> </tr> <tr> <td align="center"> <img width="1136" alt="Mathematics in Lean - Paperproof" src="https://github.com/user-attachments/assets/432dd171-faf8-42c1-a4c2-4d5f62672ff1"> </td> </tr> <tr> <td align="center">Mathlib <br/>(mathlib4/Mathlib/Algebra/Field/Power.lean:30)
</td> </tr> <tr> <td align="center"> <img width="1042" alt="Mathlib - Paperproof" src="https://github.com/user-attachments/assets/05a69569-3370-4f4e-b50b-aef7a41d50f5"> </td> </tr> <tr> <td align="center">Hitchhiker's Guide to Logical Verification <br/> (Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg) <br/> (logical_verification_2023/blob/main/lean/LoVe/LoVe05_FunctionalProgramming_Demo.lean:316)
</td> </tr> <tr> <td align="center"> <img width="1207" alt="Hitchhiker's Guide to Logical Verification - Paperproof" src="https://github.com/user-attachments/assets/4b04b1a9-ddf9-4994-b9ca-a24611a3eb93"> </td> </tr> </tbody> </table> </details>Installation
-
Install the "Paperproof" vscode extension (link).
-
In your
lakefile.toml, write:[[require]] name = "Paperproof" git = "https://github.com/Paper-Proof/paperproof.git" subDir = "lean" rev = "main" -
Then, in your terminal, run:
lake update PaperproofNote: if you're getting "error: unexpected arguments: Paperproof", it means you're on the older version of Lean, and it doesn't support per-package updates. In that case, just run
lake build. -
In a Lean file with your theorems, write:
import Paperproof -
You're done!
Now, click on the paperproof icon (after you installed the Paperproof extension, it should appear in all
<img width="200" src="https://github.com/Paper-Proof/paperproof/assets/7578559/fd077fbe-36a3-4e94-9fa8-b7a38ffd1eea"/>.leanfiles), this will open a Paperproof panel within vscode.You can click on any theorem now (well, only tactic-based proofs, those starting with
by, are supported now) - you should see your proof tree rendered.
[!TIP] If you get a build error when you try to build the paperproof package, please copypaste the error message and create the corresponding issue in Paperproof. Lean updates its metaprogramming api frequently - we try to go along with it, and it's helpful when incompatibilities are discovered on time.
The quickfix for any Paperproof build error is to use the Lean version mentioned in Paperproof's lean-toolchain.
Tutorial
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.
<details> <summary> Paperproof walkthrough </summary> <table> <tbody> <tr> <th>Lean</th> <th>Paperproof</th> </tr> <tr> <td colspan="2" align="center"> <b>Hypotheses are displayed as green nodes, <br/>goals are displayed as red nodes,<br/>tactics are displayed as transparent nodes with dashed borders.</b> </td> </tr> <tr> <td align="center"> <img width="204" alt="image" src="https://github.com/Paper-Proof/paperproof/assets/7578559/afc8000f-ad15-4ed4-b1fa-6740745895c6"> </td> <td align="center"> <img width="360" alt="image" src="https://github.com/user-attachments/assets/28605079-847b-4353-a6bf-3f668829ff97"> </td> </tr> <tr> <td colspan="2" align="center"> <b>A proof should be read "towards the middle".</b><br/> So, hypotheses should be read from top to bottom; and goals should be read bottom up. </td> </tr> <tr> <td align="center"> <img width="308" alt="image" src="https://github.com/Paper-Proof/paperproof/assets/7578559/2bd007e9-6fb3-4f32-a17d-d010af53a798"> </td> <td align="center"> <img width="366" alt="image" src="https://github.com/user-attachmRelated Skills
node-connect
337.3kDiagnose OpenClaw node connection and pairing failures for Android, iOS, and macOS companion apps
frontend-design
83.2kCreate distinctive, production-grade frontend interfaces with high design quality. Use this skill when the user asks to build web components, pages, or applications. Generates creative, polished code that avoids generic AI aesthetics.
openai-whisper-api
337.3kTranscribe audio via OpenAI Audio Transcriptions API (Whisper).
commit-push-pr
83.2kCommit, push, and open a PR
