Proposing a universal algebra exploration using Lean

Stream: general

[Terence Tao]

Hi, I have started a discussion on my blog on the possibility of launching a collaborative project to map out the implication geometry of various equational laws in universal algebra, using Lean to verify all contributions. There is a rudimentary github (currently without any blueprint or CI) with some initial Lean proofs of implications between 11 test equational laws here, but the plan is to scale this up to a much larger set of equations.

I would be interested in any thoughts on how best to set up this project. One obvious thing is to request a dedicated stream on this Zulip to coordinate the Lean-theoretic components of the project. Another obvious thing would be to set up a blueprint, though I plan to scale this project up to thousands of equations, and potentially tens of thousands of implications, and I am not sure that the existing blueprint software is ideal for this sort of size (and so a more rudimentary lightweight model might be better). Any comments would be greatly appreciated, either here or on my blog)!

[Shreyas Srinivas]

I believe that the guided equality saturation paper authors are on this Zulip and this project could potentially benefit from their work. I can't immediately find their repo on my phone. CC: @Andrés Goens

[Adam Topaz]

A little while ago I worked on the formalization of Lawvere theories in Lean, and I think this general framework could be one way to set up this project on the formal side. After all, Lawvere theories are just a categorical formulation of universal algebra. As I understand it, what this project proposes is to map out morphisms between Lawvere theories which have a presentation with one sort, one binary operation, and some arbitrary (finitely many) relations. (Of course, once the general framework is set up, there is a priori no need to restrict to just one sort and/or one operation.)

[Adam Topaz]

As for generating blueprints, it would also be possible to generate just graphs illustrating the various implications, on the fly (e.g. using Lean). There is a draft PR on the proofwidgets repo with a demo that generates (and displays) a graphviz graph constructed on the fly from some expressions. In principle the same could be done in this project -- some metaprogramming could extract all the implications that are available in the project, and generate a graph without any need to have humans write latex.

[Shreyas Srinivas]

Also, I think the data structure you are looking for is an e-graph : https://en.wikipedia.org/wiki/E-graph

[Andrés Goens]

Shreyas Srinivas said:

I believe that the guided equality saturation paper authors are on this Zulip and this project could potentially benefit from their work. I can't immediately find their repo on my phone. CC: Andrés Goens

Thanks! The relevant repo is here, which @Marcus Rossel improved a lot over the prototype we had in our paper

[Shreyas Srinivas]

I like the tactic name egg (it's like you are egging on the saturation algorithm to reach the next milestone)

[Terence Tao]

Adam Topaz said:

A little while ago I worked on the formalization of Lawvere theories in Lean, and I think this general framework could be one way to set up this project on the formal side. After all, Lawvere theories are just a categorical formulation of universal algebra. As I understand it, what this project proposes is to map out morphisms between Lawvere theories which have a presentation with one sort, one binary operation, and some arbitrary (finitely many) relations. (Of course, once the general framework is set up, there is a priori no need to restrict to just one sort and/or one operation.)

Actually for this project I'm just focusing for now on theories with a single relation, rather than many. This of course will exclude a lot of interesting theories, but I wanted to keep things as simple as possible for the pilot project and expand later. For instance, this has already allowed for a way to assign a standard name to every single theory under consideration: https://github.com/teorth/equational/blob/master/scripts/equations.txt

Regarding using Lawvere theory: I know it is the Mathlib way to abstract one's way to as broad a framework as possible, but one of the aims of my project is to involve the broader math-adjacent community, and I would like to keep the level of mathematical sophistication as low as possible, at least for the pilot project. So if possible I would like to keep the front end of the project at least free of advanced mathematical terminology, though certainly any contributor would be free to use whatever tools they wish to fill in any of the implications. So one could imagine having some API for Lawvere theories as an import that some contributors could use if they wished, but I would like to retain the ability for someone with minimal training in mathematics and/or Lean to be able to contribute a small proof to this project.

[Andrés Goens]

I think we would be very happy to see how useful this is/how far we can get with it (can't speak for @Marcus Rossel but I hope/imagine he'd like that too). For context @Terence Tao this connects Lean to a specialized “good old-fashioned” automated prover as you call it in your blog post and reconstructs a proof for Lean, it's specialized for equational reasoning. The idea/goal we had in the paper was to be able to reconstruct the equational reasoning we normally do in pen- and paper where we skip a bunch of steps, so it's kind of like calc and simp but more powerful

[Terence Tao]

It sounds like there might be enough interest to set up a dedicated Zulip stream for this topic (let's call it "Equational" as a working title). I forget who I should contact to request one?

[Shreyas Srinivas]

CC: @Johan Commelin

[Adam Topaz]

Completely understood. I'll sketch out what the general Lawvere stuff looks like in the special case of magmas with one relation

[Shreyas Srinivas]

If Johann isn't available, then maybe we should CC @Rob Lewis

[Adam Topaz]

I should be able to create a channel. Give me a few secs to recall how to do it :)

[Matthew Ballard]

Yes, any >= mod can do it

[Shreyas Srinivas]

Oh that's nice. I wrongly thought that privilege was reserved for admins

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/channel.20events/near/472926496

[Joachim Breitner]

Specific examples of magmas, such as the natural numbers with the addition operation, obey some set of equations… but not others, and so could be used to generate a large number of anti-implications.

I guess “specific examples“ could also include “all magmas up to size n” (where n is probably no more than 3, given that $3^{3\cdot 3}=19683$). I wonder how if that would be useful, or if most of these random magmas simply don’t satisfy any interesting equation.

[Terence Tao]

Joachim Breitner said:

Specific examples of magmas, such as the natural numbers with the addition operation, obey some set of equations… but not others, and so could be used to generate a large number of anti-implications.

I guess “specific examples“ could also include “all magmas up to size n” (where n is probably no more than 3, given that $3^{3\cdot 3}=19683$). I wonder how if that would be useful, or if most of these random magmas simply don’t satisfy any interesting equation.

Part of my intention of this project is to gather some empirical data to help answer these sorts of questions (in this case, "how useful are random finite magmas for distinguishing different theories?"). I kind of view the ostensible goal of working out the implication poset as sort of a MacGuffin, to help discover other interesting math and interesting workflows.

[Andrés Goens]

Shreyas Srinivas said:

I like the tactic name egg (it's like you are egging on the saturation algorithm to reach the next milestone)

it comes from the underlying reasoning engine we're using, which is called e-graphs good