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 & Lean library, open any .lean file of yours, and see your proof render as you type.
Read installation instructions →