Email Gateway (Nov 14 2021 at 01:06): Email Gateway (Nov 14 2021 at 01:06):From: Talia Ringer <tringer@cs.washington.edu>
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
Last updated: Jul 15 2022 at 23:21 UTC