Paperproof
A new proof interface for Lean 4.
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 wellknown repos.
Common tactics
Lean  Paperproof 

apply 



have  


intro  


rw  


by_contra  


use  


induction  


cases  







Fullfledged proofs
Mathematics in Lean (Jeremy Avigad, Patrick Massot) 
Hitchhiker's Guide to Logical Verification 
Installation

Install the "Paperproof" vscode extension (link).

In your
lakefile.lean
, write: if you are on a Lean version >= 4.12.0: require Paperproof from git "https://github.com/PaperProof/paperproof.git"@"main"/"lean"  if you are on a Lean version <= 4.8.0: require Paperproof from git "https://github.com/PaperProof/paperproof.git"@"21e4ec999c23fc6181d6528cbaecb600a2db6851"/"lean"
Note: if you are on a Lean version inbetween these two versions, one of these lines should work.

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 perpackage 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 tacticbased 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 leantoolchain.
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.
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. 

Nodes becomes transparent when they are not in scope. So, an opaque red node represents a currently focused goal, and opaque green nodes represent currently available hypotheses. 

Updating
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 lakemanifest.json
and lakepackages
for you.
About Paperproof
Theoretical:
 Paperproof ♥️ Semantic Tableaux: link
 Paperproof ♥️ Natural Deduction: link
 Paperproof ⚔️ Lean's #explode: link
 Lean ⚔️ Coq ⚔️ Metamath ⚔️ Isabel proof trees: link
Practical:
 How to add my Lean repo to Github Codespaces: link
 Can Paperproof render proof terms: link
 How to parse the InfoTree: link
Videos:
 a super quick 1minute demo of Paperproof: youtube link
 our Lean Together presentation: youtube link
 a full Paperproof tutorial: youtube link
Development
You're welcome to contribute to Paperproof, see the instructions in CONTRIBUTING.md.