Lean, Coq and other proof assistants: Visualising proofs as 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 ot...