The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

You might enjoy combinatorial species (and the related topics of F-algebras and polynomial functors). I’m on mobile but a quick search should yield an abundance of material.

Sent from my iPhone

On Nov 13, 2021, at 5:06 PM, Talia Ringer <tringer AT cs.washington.edu> 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

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