ProofViz: An Interactive Visual Proof Explorer (TFP 2021).
Stephen Chang, Daniel Melcer.

[  pdf  | ACM link  | Springer link  | code  | talk  ]

We introduce ProofViz, an extension to the Cur proof assistant that enables interactive visualization and exploration of in-progress proofs.

The tool displays a representation of the underlying proof tree, information about each node in the tree, and the partially-completed proof term at each node.

Users can interact with the proof by executing tactics, changing the focus, or undoing previous actions.

We anticipate that ProofViz will be useful both to students new to tactic based theorem provers, and to advanced users developing new tactics.