paperproofA proof tree for every
Lean theorem.
Lean proof is a list of tactics. Lean's default interface shows available goals and hypotheses after a single tactic.
Paperproof shows the entire proof, the way a mathematician would sketch it on paper.
Mathematics is about hypotheses and goals.
A list of tactics is barely helpful in understanding the mathematical content behind the proof. In order to read a Lean proof, we have to inspect the proof state (hypotheses and goals) after every tactic.
Paperproof shows how hypotheses and goals were transforming throughout the proof, laid out in a consistent spatial notation, so that structure and dependencies is something you simply see.
... intro h1 rw [mem_inter_iff] at h1 rw [add_comm] at h1 ...
Three boxes. Learn it in one glance.
The entire visual language is small enough to learn in a glance - colour tells you what a fact is, position tells you where it came from.
Hypothesis
Everything we know: variables, assumptions, and facts derived during the proof.
Goal
What's left to show. Close every goal and the theorem is done.
Tactic
A verb. Tells us what action transformed one Hypothesis/Goal into another.
See your next proof
in two minutes.
Install the Paperproof VSCode extension, open any .lean file of yours, and see your proof render as you type.
Read installation instructions →