The Coq mailing list

[Eduardo Ochs <eduardoochs AT gmail.com>]

Hi Talia,

I have this paper about a way to develop visual intuition about
Heyting Algebras,

  "Planar Heyting Algebras for Children"
  http://angg.twu.net/math-b.html#zhas-for-children-2
  http://angg.twu.net/LATEX/2017planar-has-1.pdf

this preprint about visualizing nuclei on Heyting algebras,

  "Planar Heyting Algebras for Children 2:
   J-Operators, Slashings, and Nuclei"
  http://angg.twu.net/math-b.html#zhas-for-children-2
  http://angg.twu.net/LATEX/2021planar-HAs-2.pdf
  https://arxiv.org/abs/2001.08338

these two preprints on visualing Grothendieck Topologies,

  "Grothendieck Topologies for Children"
  http://angg.twu.net/math-b.html#2021-groth-tops
  http://angg.twu.net/LATEX/2021groth-tops-children.pdf
  https://arxiv.org/abs/2107.11301

  "Each closure operator induces a topology
   and vice-versa (“version for children”)"
  http://angg.twu.net/math-b.html#clops-and-tops
  http://angg.twu.net/LATEX/2020clops-and-tops.pdf
  https://arxiv.org/abs/2107.11301

and this preprint on the general technique behind all this material -
a technique for doing proofs in several styles in parallel: the proof
in the usual textual form, the proof as diagram, a proof "for
children" that is a diagram for a particular case that motivates the
general case, and a formalization of the proof in Type Theory:

  "On my favorite conventions for drawing the
   missing diagrams in Category Theory"
  http://angg.twu.net/math-b.html#favorite-conventions
  http://angg.twu.net/LATEX/2020favorite-conventions.pdf
  https://arxiv.org/abs/2006.15836

I've never been able to learn Coq properly but I am rewriting/have to
rewrite the last preprint to submit it for publication before the end
of the year, and this rewriting will include converting the pseudocode
sections 6.4 and 7.1 to real Agda code... I think that this may be
close to what you are looking for.

  Cheers, =)
    Eduardo Ochs
    http://angg.twu.net/

On Sat, 13 Nov 2021 at 22:06, 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