The Coq mailing list

[Cyrus Omar <comar AT umich.edu>]

I don't have a particular idea, but you might want to reach out to Katherine Ye at CMU, whose work on Penrose is all about domain-specific visual representations of mathematical structures.

If you want these visual representations to be interactive, we've been doing some work in that area in the context of functional programming: https://hazel.org/papers/livelits-paper.pdf.

Cyrus

On Sat, Nov 13, 2021 at 10:28 PM Ralf Jung <jung AT mpi-sws.org> wrote:

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