The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Talia,

I am not sure if that is what you are looking for, but "Ribbon proofs" is an 
interesting way to visualize the structure *of* a proof:
https://johnwickerson.github.io/papers/ribbons_esop13.pdf
The paper formalizes the "syntax" of these visualizations and proves things 
about them.

; Ralf

On 13.11.21 20:06, Talia Ringer wrote:
> Hi all!
>
> I had a fun idea today for programmable neurosymbolic proof automation based on 
> domain-specific visual representations of structures. By visual representations 
> I mean representations like those seen in this blog post: 
> https://www.daniellitt.com/blog/2020/12/26/the-geometry-of-the-sylow-theorems 
> <https://www.daniellitt.com/blog/2020/12/26/the-geometry-of-the-sylow-theorems>
>
> I'm really curious if people have other domain-specific visualizations of 
> structures they reason about in proofs, especially if coupled with formal proof 
> developments! I'm extra curious when you use the visualization to reason about 
> the proofs by hand, but encode them formally in a proof assistant. I'm extra 
> extra curious if the visual representation is of a structure used inside of a 
> program, and not "just" a mathematical proof, but I'm very open to both.
>
> If you do, I'd love examples!!! This idea is like a couple of hours old, but I 
> want to write it up with some examples so I can get a sense of how tractable it 
> is, and probably propose it to some students next year.
>
> Thanks!
>
> Talia

--
Website: https://ralfj.de/research