coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Domain-specific visual representations of structures for proofs

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr, cl-isabelle-users AT lists.cam.ac.uk
Subject: [Coq-Club] Domain-specific visual representations of structures for proofs
Date: Sat, 13 Nov 2021 19:06:15 -0600
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mx6.cs.washington.edu
Ironport-hdrordr: A9a23:p7+nuKn5fJX6Lwcj8Uk4oZUgNajpDfIA3DAbv31ZSRFFG/Fw9vre5cjzsCWftN9/YgBDpTntAtjifZq+z/5ICOsqTNOftWDd0QPCQe1fBODZslrd8kPFh4hgPGRbHJRWOZnfCVB7iILd+wm3E9EpxZ2i/LqzjenTi1dBJDsaDp2IIz0WNu9TKCxLeDU=
Ironport-phdr: A9a23:Jd6UzBMOsaebugfhtDol6naCDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r3QaCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fXbglVizawYbF/JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4LpxSBLwhygJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRfDIyma4sPDvAONvtEoYn8oVsOogWxBROxD+7o1j9InH723as10+s/CwHLxxAvH8kUvHXattr1L6cSUeGzzKnH0TXDaPVW1S3j54fVbxAsuPeBVq9/fsTN00cgDR/FjkmOpoz/OTOYzuQAvmuU4uZ9SO6iim4qpQFtrjWt28oglpTFi4YaxF7K6Ch0z5o5KNykREN5btOpEIZcuzyUOoZrRs4vTW9ltSc8x7Ybt5C7ey0Kx44mxx7Zc/GIbpKH4hTiVOmPJTd4gHNleK6jhxqo7Uegzej8W8+p21hJtipIisTAum4O2hDJ9MSLVvhw8l2u1DuNzQze6vxILVgqmabHL5Mt2L09m5oJvUjeHyL7mV/6ga+Kekgi5+Om8f7oYq/8qZ+ZL4J0ih/xMqApmsGnBOQ5PQkDU3KH9uSnzrHi81f2QK5Kjv03lKnZv4zaJcMdpqKjHQBaz5sj5w6+DzegztsYgWEKIE9bdB+ElYTlJU3CLfPiAfqwgVmgijdmy+3eMr3kGJrNL3zDkLn7fbZ67k5R0BYzzcpe55JSBbEOPujzV1Ttu9zDFBM4PRa7w/3nCNV80IMeVn6PAqifMK/Ir1CH+/8vL/GWZIAJoDb9N+Ql5/n2gHAlnl8dZLCl0ocTaHClBftrOF6ZYHrpgtcZC2gGpAs+TOrwiF2DSzFffXiyX7hvrg08XYmhFMLIQp2nqL2HxiayWJNMIihNDhWNCn7ieoGAVrIRcy+IOedlkycYTv6qQopn3BroqQyp5aBgK7/o8ykZvNrZ1d566vebwQ0o9Dp7At612HrLUGhvnmIOSCMx2uZyrVErmQTL6rRxn/ENTY8b3PhOSApvbfY0KsRxEJbtUxnBf9GGVFGgBNiqHGNpJjrQ69oePQB2AJO9hwvD3iylH7gT0bGHGc5smkoz93PqYdl00HbH0qY9iF9gT8dSZzTOuw==

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

[Coq-Club] Domain-specific visual representations of structures for proofs, Talia Ringer, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Timothy Carstens, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Eduardo Ochs, 11/14/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Ralf Jung, 11/14/2021
  - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Cyrus Omar, 11/14/2021
    - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Lawrence Dunn, 11/15/2021
- Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Clément Pit-Claudel, 11/15/2021
  - Re: [Coq-Club] Domain-specific visual representations of structures for proofs, Jim Fehrle, 11/15/2021