Is there a visualizer of proofs?

Stream: new members

[Yuetong Zhang]

For example, to prove the commutativity of addition, in Lean we have

theorem add_comm (a b : ℕ) : a + b = b + a := by
induction a with a ha
rw [zero_add]
rw [add_zero]
rfl
rw [succ_add]
rw [add_succ]
rw [ha]
rfl

In my mind, there should be a diagram (types omitted)
b = b...................a + b = b + a
....↓.................................↓
b = b + 0.............succ (a + b) = succ (b + a)
....↓.................................↓
0 + b = b + 0.......succ (a + b) = b + succ a
....↓.................................↓
....↓....................succ a + b = b + succ a
......↘............................↙
...(by induction) a + b = b + a
This is basically the goals written backwards (but since not all lean codes are backwards, they might not be always so). Now, do we have some tool to make the lean code into this "math style" "chain of propositions" diagram, or even one which we can interact with by drag with our mouse or like?

[Marc Huisinga]

I think https://github.com/Paper-Proof/paperproof is the closest to what you are looking for

[suhr]

There's also https://github.com/nomeata/lean-calcify

[Aaron Liu]

There's also #explode (in file#Tactic/Explode)

[Julian Berman]

And there's also also David Renshaw's https://github.com/dwrensha/animate-lean-proofs