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.
We created a few videos about Paperproof:
- a super quick 1-minute demo of Paperproof: youtube link.
- our Lean Together presentation: youtube link.
- a full Paperproof tutorial: youtube link.
Here you can read about Paperproof in context of other proof trees: lakesare.brick.do/lean-coq-isabel-and-their-proof-trees.
And here you can read how Paperproof analyzes Lean's InfoTree to build the trees you see in the user interface: link.
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
Full-fledged proofs
Mathematics in Lean (Jeremy Avigad, Patrick Massot) |
Hitchhiker's Guide to Logical Verification |
-
Install the "Paperproof" vscode extension (link).
-
[TEMPORARY STEP] Downgrade "lean4" vscode extension to version
0.0.144
Explanation: Paperproof depends on
lean4
extension in order to avoid loading your computer with excessive Lean server instances; howeverlean4
api regularly updates in a way that introduces breaking changes, resulting in a blank screen in Paperproof. Hopefully their api stabilizes soon and we can remove this step, but at the moment - please downgradelean4
, and turn off automatic extension updates forlean4
. -
In your
lakefile.lean
, write:require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean"
-
Then, in your terminal, run:
lake update Paperproof
Note: 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
.lean
files), 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.
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
To update Paperproof, you only need to rerun lake update Paperproof
. This will fetch the newest version of the Paperproof Lean library from this github repo, and build it.
Vscode extensions are automatically updated, however you can check for new updates with
cmd+shift+p
=> "Extensions: Show Extension Updates".
Paperproof is a package that's usually only used during development, so you might want to remove it from your lakefile.lean
when you're pushing to production. In order to do that, just remove the Paperproof require from lakefile.lean
, and run lake update Paperproof
. This will clean up lake-manifest.json
and lake-packages
for you.
You're welcome to contribute to Paperproof, see the instructions in CONTRIBUTING.md.