Back

@tao The universal algebra community has had tools for this for sort of thing for a long time. For instance, you can check out https://www.cs.unm.edu/~mccune/prover9/. It would be interesting to see more continuous methods like neural nets combined with tools like these to impart some more human intuition. I was actually asking @ProfKinyon about this earlier this month.

@caten @tao Yeah, once candidate identities are given, any automated theorem prover can handle the task of sorting out how different varieties (in the universal algebra sense, i.e., equational classes) are contained in other varieties. Generating the candidate identities (subject to reasonable constraints) would be the other part of it.

@ProfKinyon @caten There is a third task here which could potentially benefit from AI tools: trying to *disprove* an implication of one identity from another by producing a magma which obeys the former identity but not the latter. One could imagine using machine learning to generate candidate magmas that are likely to achieve this goal, and then using an SMT solver or something to formally verify.

A fourth task that is rather vague, but perhaps closest to replicating human intuition, is to develop some way of automatically assessing whether a given identity (or conjunction of identities) is "strong" or "weak", either in absolute terms or relative to some other collection of identities, allowing one to possibly strategize proofs or disproofs of implications by splitting the task into smaller pieces, as I discussed in a recent post.

@ProfKinyon @caten Perhaps I can pose a concrete challenge to focus the discussion. Consider the collection of all possible universal equational laws in which the magma operation + is applied at most four times. For instance, the associative law (𝑥+𝑦)+𝑧=𝑥+(𝑦+𝑧)) is of this form. I don't know exactly how many such laws exist, up to relabeling and symmetries, but let's say for sake of argument that there are around a thousand. The (admittedly artificial) challenge is to completely specify the partial ordering on this collection given by implication, thus extending the diagram included here to the other thousand or so identities involving at most four operations. Is this feasible to accomplish by some combination of current automated tools and reasonable number of human expert-hours? Note that one has not only to prove those implications that happen to be true, but also to disprove those implications that happen to be false. One could blindly throw random implications into various automated theorem provers, but would it actually be computationally feasible to completely specify the million or so implications this way? Or would some sort of automated "intuition" coming perhaps from machine learning tools be a significant speedup?

@tao @ProfKinyon As far as the number of such equations goes, the number of bracketings of n variables is given by the Catalan numbers, so you could likely give the exact count of the number of formulas of a certain size in terms of those and any symmetry you want to quotient out by, assuming you were okay going by the number of variables appearing rather than the height (number of applications of the operations). Similar ideas should work for counting by height instead, I'd imagine.

Anyway, my initial guess is that this task has a chance of being undecidable in general. I don't have a proof, but some similar tasks are impossible. First, there are finite magmas that generate varieties which are not finitely based (i.e. there is no finite list of equations which imply all others that are true for the magma). Second, some varieties have an undecidable equational theory (i.e. there cannot exist an algorithm for checking whether a general equation is true in that variety). Third, the lattice of clones on a set with even three elements is already uncountable. While you would only have us look at a finite fragment of a countable part of this lattice (the varieties axiomatized by a single identity), I feel unsure that such an algorithm can exist.

This isn't to say that you couldn't typically make the decision, but I also wouldn't bank on it being effectively solvable for all relatively small equations.

@caten @ProfKinyon It looks a bit more complicated to me than Catalan numbers due to the ability to repeat variables, but certainly I could imagine a brute force search could enumerate these formulae reasonably quickly. (I am somewhat tempted to try out GPT-4's vaunted code generation ability for this task, though I foresee that debugging such AI-generated code could be more time-consuming than writing the code by more traditional means.)

I agree that likely there will be undecidable implications at some point. But perhaps a reasonable goal is to have automation work out the truth or falsity of, say, 90% of all possible implications, and then of the remaining 10%, isolate the most "interesting" or "critical" 1% to then pose to human experts. Perhaps humans can resolve all but 0.1% of these critical implications, which one can then pose as open conjectures. [These percentages are completely made up, of course.]

I also have the hope that even just having 90% of the implication graph might reveal some interesting features that would not have been obvious to human experts who might only encounter O(1) of these equational laws at a time, and were previously not able to explore the more global structure of the space of laws. (For instance, is there a phenomenon similar to that in reverse mathematics where many arithmetic theories seem to collapse to one of the "big five"?)

@tao @ProfKinyon I was originally going to say that I wouldn't be surprised if this was the case, but the more I think about it the less sure I am. It's true that while universal algebra has at this point considerable tools for handling arbitrary varieties of algebras, most of the ones people actually study are either "like groups" or "like lattices". One idea is that the ones that are too alien are too degenerate, but it could also be that studying them is too hard, even with computer help, so we will always be stuck in the small tractable region we have already found.

It is true that a randomly-chosen finite algebra will be primal with probability 1 (Murskiĭ's Theorem), so most finite algebras can be thought of as basically identical from an equational perspective, up to relabeling the basic operations. However, the number of algebras grows very quickly up to isomorphism, so checking whether a given algebra is "trivial" in this sense may rarely be attainable. See https://www.ams.org/journals/proc/1966-017-03/S0002-9939-1966-0200219-9/S0002-9939-1966-0200219-9.pdf.

@tao @ProfKinyon This has been really neat btw! I'm going to have to drop off for now as I will be in big trouble if I don't post a particular preprint to the arXiv in the next eight hours or so lol.

@tao Ruler I think is also lossy wrt the relationships between equivalent rewrite rules since it treats them all as the same, but this is solvable since it's possible to track proof information inside of the underlying data structure, it was just not needed for this purpose.

@tao @caten Regarding Terry's "concrete challenge", I have the following feeling after having played around with the program Prover9/Mace4, that Charlotte mentioned, on other problems. The program is good at finding small counterexamples when they exist. It is also good at finding proofs of an identity inside a given variety, when the number of identities defining the variety is small, and when the identities are simple.

In the stated challenge, the poset is limited to pure equational theories in a single operation, each involving only a single identity of a very small length. So I expect that a brute force approach would work to handle a significant number of the cases.

I believe it would be quite possible to train a machine to look for proofs and counterexamples, in a more efficient fashion. Currently, Prover9 can struggle, even when guided, to find a simple argument when the varieties get more complicated. (In the paper https://link.springer.com/article/10.1007/BF01772930 it is proved that *-regular rings are *-finite. My attempts to direct Prover9 to discover the next step in the proof led to it getting stuck.)

Charlotte mentioned the issue that equations can have infinite models but no nontrivial finite models. I know of no existing computer tools that help in overcoming this issue. Indeed, that sort of problem is what makes a large part of my own research difficult/interesting. Still, if a student took up Terry's challenge, it would be quite interesting to discover new examples (possibly simpler than any existing examples) where an algebra satisfying one simple equality but not another had to be infinite.