[butokai]

For the Coq proof assistant, a recent approach to graphical proofs is Actema: https://www.actema.xyz/