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 ot...