Lean/Coq/Isabel and Their Proof Trees

This week we (me & Anton Kovsharov) published Paperproof, a Gentzen-tree-like proof interface for Lean 4. In this post I'll review proof visualisations from other proof assistants, as many as I can find.
Send more my way if you know of any others, I'll happily incorporate them into this post.

In this review we're considering proof visualisation tools that were created with actual mathematicians in mind - tools that are supposed to make formalising mathematics (and parsing existing mathematical proofs) in proof assistants easier. 

It just so happens, that such tools always visualise tactics proofs as a tree (really we'd be thrilled if you can think of any other shape that helps us grok the structure of the proof). So, in this review, I'll focus on interfaces that at least remind us of sequent-calculus-style trees.

There exists one other sort of tools which are frequently called proof visualisers - programs that simply display a tactic state before and after each tactic application. Examples of such tools are Coq's Alectryon, Lean's LeanInk and Coq's Coq-psv. These are great for rendering proof assistant documentation & theorems in mathy blog posts, but they don't offer any additional value in writing proofs or parsing the structure of existing proofs, so we're not considering these tools here.

We are also not considering proof interfaces that are designed for learning logic and can't be used by real mathematicians working on formalizing mathematics, such as ProofWeb or Incredible Proof Machine.

Lean

Paperproof (by Evgenia Karunus & Anton Kovsharov)

So, our tool. Paperproof is available as a VSCode extension, and can only be used with Lean 4. 

On the screenshot you see how Paperproof will render a Lean tactic proof (seen on the left side of the screen). You can also check out a video we made to see how this tree gets constructed in real time.

Hypotheses are displayed as green nodes, goals are displayed as red nodes, tactics are displayed as transparent nodes with dashed borders. If you drag these nodes around you will see arrows, however we're not displaying them to clean up the interface.
Slightly darker backgrounds demarcate variable scopes - you can only use hypotheses that are outside of your box, you can never dive into some new box. Don't overthink this however, we'll always highlight the available hypotheses as you're writing the proof, consider backgrounds a visual hint that will eventually become second nature.

We start from our goal s ∩ t = t ∩ s, write tactic ext x, which turns our goal into x ∈ s ∩ t ↔ x ∈ t ∩ s.
Then we write the tactic apply Iff.intro, which turns our goal into 2 goals - naturally, this is displayed as a tree bifurcating into two nodes.
Note how goal nodes always form a tree. 
Hypotheses form similar trees, e.g. rw [Set.mem_inter_iff, and_comm] at h1 turns h1: x ∈ s ∩ t into h1: x ∈ s ∧ x ∈ t, and then into h1: x ∈ t ∧ x ∈ s.

Aside: the fact that goals nodes form a tree is a consequence of how Lean and other proof assistants handle goals. Goal nodes form a tree because expressions in programming languages form a tree, and writing tactics is nothing other than gradually assigning some expressions to these nodes.
Hypotheses, however, do not have to form a tree. It's perfectly possible that a hypothesis a ∧ b bifurcates into a and b, but it's equally possible that a and b would unite into a ∧ b! It's possible to write such a tactic. Empirically, however, that never happens in Lean - all tactics we observed only went one way (from a single initial hypothesis to multiple hypotheses).
So, fundamentally, goals form a single tree, - and, empirically, hypotheses form many little trees.

Coq

ProofTree (by Hendrik Tews)

ProofTree is the oldest tool on the list, it was first released in 2011. ProofTree can only be used with Coq and in ProofGeneral (that's emacs editor for Coq).

ProofGeneral's ProofTree is similar to Paperproof conceptually (just revert it upside down to see it!), except ProofTree shows ⊢ instead of goal types, and doesn't display hypotheses at all.

Displaying hypotheses and variable scopes is hard work, however displaying goal types should be straightforward, wonder why he decided against that.

Traf (by Hideyuki Kawabata)

Here we get to something! Traf is ProofTree's posterity, and it was developed as an extension of ProofTree.  Like ProofTree, it's Coq-only tool that can only be used via ProofGeneral. It's pretty similar to Paperproof, and should be worth trying if you're in Coq.

Traf offers a veridical recreation of Gentzen trees, as Hideyuki puts it:

Traf is different from ordinary proof viewers and proof translators in that it is designed to guide interactive theorem proving by using a full-edged proof assistant through a standard tactic-based interface. In other words, Traf is a helper tool for enhancing both the writability and readability of proofs. The proof tree shown in Traf's window looks like a readable Gentzen-style natural deduction proof. 

One way in which Paperproof took a route different from Traf's is the displayal of hypotheses - Traf only displays the hypothesis once the goal is closed (and duplicates reused hypotheses, just like in Gentzen trees!), and Paperproof treats hypotheses as separate trees - it shows their history, shows what hypothesis originated from what hypothesis, and in what scopes they were available throughout the proof.

PeaCoq (by Valentin Robert)

PeaCoq is available as a locally hosted web app, and only works with Coq.

PeaCoq superficially looks like a proof tree, however what you see as a "tactic state [aka goal] forking into 2 tactic states [aka goals]" is not that. PeaCoq shows the current proof state on the left, suggests multiple tactics, and shows what the results would be on the right.

What PeaCoq is most similar to is Lean's default infoview diffs (where the changed subexpressions in hypotheses/goals are highlighted).

Isabelle, Metamath, Agda

Nothing? I couldn't find anything resembling proof visualisations for these proof assistants. Send some my way if you know of any.

Conclusion

I fully expected to continue writing this post for many pages more - after all, other than Lean, I've only dealt with Coq! But no - sorry for the abrupt end, it seems like among all proof assistants and among all proof visualisers there are only two realistic tools for the job:
Traf if you use Coq (should work) and
Paperproof if you use Lean 4 (will certainly work).