[isabelle] Domain-specific visual representations of structures for proofs

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

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.