Apart from the default Infoview, Lean has two proof visualisations:
Let's see how both of these render the very same proof:
theorem hi (a b : Prop) : a ∧ b → b ∧ a := by
intro ab
cases' ab with hA hB
apply And.intro
exact hB
exact hA
#explode
is a command in Mathlib. You can use it by importing the relevant file with import Mathlib.Tactic.Explode
, and writing #explode yourtheoremname
.
See the example output below:
Paperproof is a vscode extension. This is how you would use Paperproof to render the same proof:
To anyone who has skimmed through a beginner logic textbook, the main difference will be apparent  #explode visualises Lean proofs as a Fitch Table, and Paperproof visualises Lean proofs as a Gentzen Tree.
What's less obvious is the fact that they use two different data structures to glean information from a Lean proof.
For any given proof statement, we have 3 options:
.lean
file as a text file. This will give us a string of tactics.Expr
 this will render your proof in terms of lambda abstractions and applications. You will get output similar to what you get when you use the #print
command.InfoTree
 this gives you a sequence of tactics that were applied in a proof. Per each tactic, you get two lists: "a list of goals and their hypotheses" before this tactic was applied, and "a list of goals and their hypotheses" after this tactic was applied.[conspiracy theory]
Hey, might it be that the "Infoview" title comes from "InfoTree" (Lean data structure that's used to glean information from the Lean proof) + "Webview" (vscode's name for the vscode panel where the Infoview and other such interfaces can be rendered).
These options and their corresponding output can be seen in the diagram below.
To drive the point home on how tragic it is to lose all tactic information, let's create our own tactic:
elab "ourOwnTactic" : tactic => do
let mvarId ← getMainGoal
let term ← `(λ a b ab => And.casesOn (motive := λ t => ab = t → b ∧ a) ab (λ hA hB _ => And.intro hB hA) (Eq.refl ab))
let expr ← elabTerm term none
mvarId.assign expr
As you see, our tactic simply assigns the entire proofterm to the theorem in one sweep.
tactic proof  proofterm proof  ourOwnTactic proof 



Three different ways to prove the same theorem that result in the very same Expr . 
So, despite the fact that vastly different code was used to prove the hi
theorem, our Expr
stays the same, and the visualisation that's based on Expr
s will render all three proofs above in exactly the same way.
Now, back to the difference between #explode and Paperproof  how do each of these glean information from the Lean proof?
#explode uses Expr
s, and Paperproof uses InfoTree
s. The only reason you seem to see a reasonably highlevel proofs in #explode is because many Lean tactics are lowlevel already (intro
is just lambda abstraction, apply
is just lambda application).
Let's summarise the situation in a table below:
lowlevel ( Expr )  highlevel ( InfoTree )  
table  ???  
tree  ??? 
So, why does #explode use Expr
s? Because there exists a way to translate lowlevel stuff (calculus of inductive constructions) into a Fitch Table interface, and there is no way to translate highlevel stuff (tactics) into a Fitch Table interface? No, #explode could potentially display both Expr
data and InfoTree
data.
The same goes for Paperproof  Paperproof could well render both Expr
data and InfoTree
data.
Mario Carneiro went for Expr
s because he specifically created #explode in order to get a glimpse into what proof term extremely highlevel tactics such as simp
result in. That's the entire purpose of the #explode command.
The reason why Paperproof uses InfoTree
s is because, like described above, it would be really tragic to lose all the tactic information. We want to display exactly the abstraction level that the proof author intended. Paperproof specifically aims to be a onetoone mapping of the proof written to the proof displayed.
[evgenia's biography]
In fact, Paperproof stumbled upon theExpr
vsInfoTree
choice early on. Before I understood I should useInfoTree
s for the Paperproof's parser, I ported the #explode command from Lean 3 to Lean 4 (link), thinking that I might build a Paperproof tree by adjusting #explode's output.
In either case, we now have two missing cells  a Fitch Table that renders highlevel details (#explode + InfoTree
), and a Gentzen Tree that renders lowlevel details (Paperproof + Expr
). Regarding the former, a PR into Mathlib might be welcome. The latter, Expr
rendering in Paperproof, would certainly be a welcome addition to Paperproof. You can read more on that in "Can Paperproof render proof terms?".