Future directions

Stream: Equational

[Terence Tao]

It is somewhat hubristic to start talking about the future of the project when it is only three days old, but I wanted to have a place to record thoughts on this topic well in advance of when they would actually become a reality.

It seems to me that once we accomplish the primary goals of this project, there are many further things one could then do with this platform and data set. So I wanted to collect ideas of what else could be done after the primary goal (and in some cases, partially concurrently with achieving that goal). Here are some suggestions to get the ball rolling:

• Explore triple relations of the form "Equation X and Equation Y implies Equation Z". This was for instance proposed by Pace Nielsen in this blog comment, and I think elsewhere as well. This will be harder for several reasons, most notably because 3-SAT is way harder than 2-SAT, but the relations we obtain in this project will help reduce the problem significantly. As Pace suggests, we may have to cut down to just three operations instead of four to obtain a feasible project.
• See if there is a shorter equation than the six-operation Kisielewicz law (((y ∘ y) ∘ y) ∘ x) ∘ ((y ∘ y) ∘ z) = x that has the property that it has non-trivial models, but that they are all infinite. (The proof of this claim been formalized in equations#58, which should be merged soon.) Presumably it will become easy to figure out which four-operation laws have finite or infinite models when our project is complete; no idea how challenging searching the five-operator space will be, though.
• Once the implication graph is complete, it would be interesting to see how machine learnable it is. Could an AI glance at an implication and make a good guess whether it is true or false?
• One could gamify some aspect of the task of completing the implication graph. One could imagine a web site that serves up a random implication or anti implication, and one has to play some version of the natural number game to resolve it. This could have some pedagogical value. (It occurs to me that this would also make a rather sadistic CAPTCHA.)

[Shreyas Srinivas]

For the the third task, I would be looking at good old fashioned AI search heuristics

[Shreyas Srinivas]

One thing about a sparsified implication graph is that there could be many sparsifications, so it would be interesting to ask what the desirable properties of a good sparsification of the implication graph are

[Shreyas Srinivas]

One property I am curious about is whether hop count in the graph is correlated with the size difference between terms.

[Shreyas Srinivas]

To state my hypotheses upfront, I expect that the automated equations searches will yield implication graphs where the correlation is high since they might use some greedy heuristics in their exploration.

[Terence Tao]

I'm hoping that once we actually have a medium sized data set of implications, we can really refine the vague intuition that domain experts have about the logical strength of typical axioms, and maybe find some useful rules of thumb for the fastest way to try to prove or disprove some implication. I'm not really an expert in the field, but I don't know of any prior experimental mathematics in this area.

[Shreyas Srinivas]

There are a few things I have in mind on that front. One is to compute a routing table for this graph. Think of it as each node maintaing a table that takes as input another node which is your goal and then tells you what your next best hop is

[Shreyas Srinivas]

The other is to check the size of cuts

[Shreyas Srinivas]

And the idea is that small cuts in the graph represent crucial sets of implications that lots of implication paths use

[Shreyas Srinivas]

I would consider these the bottleneck theorems that proof searchers should seek out.

[Shreyas Srinivas]

And then the question is : empirically how would a random walk on the graph perform depending on the smallest cut between a source node and a target node.

[Shreyas Srinivas]

Anyway this is speculative. I just want an excuse to run some Markov process on a real data set

[Terence Tao]

It's astonishing actually how many fields of mathematics have virtually no sizeable data sets. (There are notable exceptions, e.g., knot theory, number theory, or the more applied parts of PDE. The OEIS in principle is a data set for all of mathematics, but primarily on the combinatorial/number theoretic side in practice.) There's a lot of types of ways of doing research that are simply not possible right now.

[Shreyas Srinivas]

In general I like the idea of actually simulating random processes. Even theoretical ones. Just haven't found the right opportunity to do it so far.

In my group one of our topics is designing fault tolerant clock synchronisation schemes. Like most algorithmists we usually prove bounds about worst case synchronisation behaviour. But our schemes don't render themselves easily to average case analysis, since they repeatedly take medians of multiple signals (continuous random variables on bounded support) copies for fault tolerance. One of my advisor's former students ran simulations for average case behaviour of one of our algorithms, and he found astonishing gaps between in the performance of the simulation and the theoretical analysis.

[Shreyas Srinivas]

That's had me wondering more about random process simulations and this data generated by equations seems like a solid reason to try it out.

[Kim Morrison]

Terence Tao said:

It's astonishing actually how many fields of mathematics have virtually no sizeable data sets.

https://mathbases.org/ is a recent attempt to index more of these. Perhaps one artefact of this project will be a "database"?

[Cody Roux]

Or indeed, a database with no quotes!

[Terence Tao]

On reading a 1997 paper of Kisielewicz https://mathscinet.ams.org/mathscinet/article?mr=1619699 I see that the first research question is solved: the shortest law that has infinite, but no nontrivial finite, models is

(((1 ∘ 1) ∘ 1) ∘ 0) ∘ (1 ∘ 2) == 0

or in equation form

(((y ∘ y) ∘ y) ∘ x) ∘ (y ∘ z) = x.

I put the proof that this is such a law in the blueprint here. (By the way, what number would we assign to this law?)

Kisielewicz was able to show that none of our 4694 equations have this property, which was a remarkable achievement using 1997 levels of computing. A couple notable tidbits from his paper:

• He mentions a 1965 result of Austin that every law that only involves two variables has at least one non-trivial finite model.
• He mentions that the law (y ∘ x) ∘ ((x ∘ z) ∘ z) = x (equation 1689) implies the singleton law x=y, but that the proof is quite lengthy. This would be a good test case for automated equation provers (or a challenge for human provers).
• He mentions that the five-operation law y ∘ (y ∘ (y ∘ (x ∘ (z ∘ y)))) = x (equation ???) has no non-trivial finite models, but it is an open question whether it has any infinite models.

[Amir Livne Bar-on]

The numbering of the order-5 laws would be
equation 28393 := x = (((x ∘ x) ∘ x) ∘ y) ∘ (x ∘ z)
and
equation 5105 := x = y ∘ (y ∘ (y ∘ (x ∘ (z ∘ y))))

[Maja Kądziołka]

Terence Tao said:

(((1 ∘ 1) ∘ 1) ∘ 0) ∘ (1 ∘ 2) == 0

or in equation form

(((y ∘ y) ∘ y) ∘ x) ∘ (y ∘ z) = y.

these are different laws. you mean ... = x?

[Andrés Goens]

(yeah, the paper he linked to also says ... = x, so surely the typo was that way around)

[Terence Tao]

Sorry for the typo, this is now fixed.

[Terence Tao]

One future research question noted in #Equational > Infinite magmas? and recorded here for easy reference: are there X, Y less than or equal to 4694 such that EquationX G ∧ ¬ EquationY G is satisfiable by an infinite magma, but not by any non-trivial finite magma? It is known that this is not possible for Y=2. X=168 (the central groupoid case) may be a promising place to start, and suggests a subproject of determining all the laws in our list of 4694 implied by Equation168.

[Daniel Weber]

Terence Tao said:

One future research question noted in #Equational > Infinite magmas? and recorded here for easy reference: are there X, Y less than or equal to 4694 such that EquationX G ∧ ¬ EquationY G is satisfiable by an infinite magma, but not by any non-trivial finite magma? It is known that this is not possible for Y=2. X=168 (the central groupoid case) may be a promising place to start, and suggests a subproject of determining all the laws in our list of 4694 implied by Equation168.

I found such a non-implication, equational#244

[Will Sawin]

I guess one can raise the question of what is the first implication which is true for all finite magmas and not provable using the axiom scheme that f ∘ g =id implies g ∘ f = id for f,g any functions defined by composing the binary operation? But maybe this question is a bit silly.

[Terence Tao]

Well, surjunctive groups are a thing, so this isn't a totally outlandish question. Perhaps there is some literature in the model theory of groups on how to discern a finite group from a more general surjunctive group... (though Wikipedia says that it is not known if there are any non-surjunctive groups, though certainly there are non-surjunctive magmas...)

[Franklin Pezzuti Dyer]

As another interesting family of results that we might consider tackling in the project, consider "non-interpolation theorems" of the form "EqX --> EqY, but there is no equation EqZ such that EqX --> EqZ --> EqY strictly".
See this MSE post for a cool example - it might be fun to try formalizing the result there.

[Will Sawin]

One area I thought may be worth investigating when the project is done is the set of neighbors in the Hasse diagram of the associativity equation (since associativity is so mathematically interesting, anything slightly stronger or weaker than associativity might also be interesting). That could be a place to start for proving non-interpolation theorems as there's a bit more motivation there than for an arbitrary pair of equations.

[Franklin Pezzuti Dyer]

Will Sawin ha dicho:

One area I thought may be worth investigating when the project is done is the set of neighbors in the Hasse diagram of the associativity equation (since associativity is so mathematically interesting, anything slightly stronger or weaker than associativity might also be interesting). That could be a place to start for proving non-interpolation theorems as there's a bit more motivation there than for an arbitrary pair of equations.

Do you know of any proven "neighbors of associativity" already from the literature? The only non-interpolation-type result that I know of currently is the one I linked

[Zoltan A. Kocsis (Z.A.K.)]

One long-term hope I had (and one reason I started contributing) is that the infrastructure built here could lead to some insights about degree of satisfiability-style results, e.g. are there non-trivial examples involving magmas satisfying only one equation?

Such results include:

1. In a finite group, either all elements satisfy $x^2 =1$ or at most $\frac{3}{4}$ of them do. Similarly, it's a classic result of Gustafson that either all pairs satisfy $xy=yx$ or at most $\frac{5}{8}$ of them do. Similarly, either all pairs satisfy $xy^2 = y^2x$ or at most $\frac{7}{8}$ of them do. These all have various analogues in infinite groups. Last time I checked it was open whether $x^p = 1$ for $p > 5$ satisfies any analogous property, or if for each $\varepsilon$ there's a finite group where the fraction of elements satisfying it exceeds $1 - \varepsilon$.
2. In a finite Heyting algebra, either all elements satisfy $x \vee \neg x = \top$, or at most $\frac{2}{3}$ of them do. The same holds for pairs satisfying $x \vee y = \neg(\neg x \wedge \neg y)$. This again has various analogues in infinite Heyting algebras. Unlike the group case, we know what happens in large one-variable equations w.r.t. this property: Bumpus and I classified all of them in this article.
3. BCK-algebras have a bunch of results analogous to what happens in Heyting algebras, proven by Evans here.

[Terence Tao]

Franklin Pezzuti Dyer said:

Do you know of any proven "neighbors of associativity" already from the literature? The only non-interpolation-type result that I know of currently is the one I linked

There's not much that's stronger than associativity. In fact the MathOverflow post that inspired this entire project was devoted to that question. @Pace Nielsen had eliminated all but a finite number of candidates, and I showed that one of the candidates actually worked. Presumably our new data will in fact give the complete list.

The question for what axioms are minimally weaker than associativity may be harder, though.

[Terence Tao]

@Zoltan A. Kocsis (Z.A.K.) If a magma of n elements (with n large) obeys a law, and one arbitrarily adds adjoins a small (bounded size) counterexample to that law (and then fills out the rest of the multiplication table arbitrarily), then the resulting combined magma will not obey the law 100% of the time, but rather by some fraction that is arbitrarily close to 100%.

However there was a result of Gowers and Long that got some weaker conclusion for magmas that partially obey the associative law: https://arxiv.org/abs/1904.08732 . Perhaps this statement has analogues for some other laws (e.g., the central groupoid law, 168).

[Zoltan A. Kocsis (Z.A.K.)]

@Terence Tao :

If a magma of n elements (with n large) obeys a law, and one arbitrarily adds adjoins a small (bounded size) counterexample to that law (and then fills out the rest of the multiplication table arbitrarily), then the resulting combined magma will not obey the law 100% of the time, but rather by some fraction that is arbitrarily close to 100%.

I think that's the answer to a different question, right? I'm looking for pairs of laws $\varphi(\overline{x}), \psi(\overline{y})$ so that if all tuples $\overline{x}$ in a magma $M$ satisfy $\varphi(\overline{x})$ then either

• all tuples $\overline{y}$ from $M$ satisfy $\psi(\overline{y})$; or else
• only some bounded fraction of those tuples satisfy $\psi(\overline{y})$.

If you start with $M$, add counterexamples to $\varphi(\overline{x})$ and obtain $M'$, that resulting $M'$ can't serve as a counterexample to the implication above since it does not satisfy the premise. In turn if you try to add counterexamples to $\psi(\overline{y})$, you have to do it in a way that does not add any counterexamples to $\varphi(\overline{x})$. (Such pairs definitely exist, take $\psi(y_1,y_2) \leftrightarrow y_1=y_2$, which is satisfied by at most $\frac{1}{2}$ of elements; I'm interested in nontrivial ones).

[Terence Tao]

Ah okay, I misunderstood what you meant by "magmas satisfying only one equation".

My candidate for $\varphi$ would be the central groupoid axiom 168, and $\psi$ one of the natural central groupoid axioms, the simplest of which is (x ◇ y) ◇ z = (w ◇ y) ◇ z (but other options are available). Knuth's paper https://www.sciencedirect.com/science/article/pii/S0021980070800321?ref=cra_js_challenge&fr=RR-1 has a lot of discussion on this; it doesn't directly address the satisfiability question but I imagine that the graph-theoretic formulations of the law in that paper might be helpful.

[Zoltan A. Kocsis (Z.A.K.)]

Thanks, this definitely looks very interesting! I am double-glad I claimed the related issue now!

[Daniel Weber]

If we start having lots of infinite models as counterexamples an interesting future direction might be seeing which implications do hold over finite models

[Terence Tao]

equational#364 will be a step in that direction, since by the Lefshetz principle, every linear counterexample can be realized over some finite field

[Cody Roux]

Noting that decision procedures are typically faster over the reals than over finite fields (though perhaps harder to implement)

[Franklin Pezzuti Dyer]

Another idea for the future could be to search for examples of implications between "simple" laws that require the largest number of steps (as measured in terms of the elementary moves used to define ⊢) to prove, given the complexity of the laws involved. Seems tricky to prove minimality/maximality for things like this, but it would be similar to the "busy beaver hunting" that people have done before

[Franklin Pezzuti Dyer]

By the way, are folks' future ideas being consolidated anywhere in the repo?

[Terence Tao]

This thread is the consolidation. There is also a stub of a section at https://github.com/teorth/equational_theories/wiki/Plan-of-paper for future directions but it is currently unpopulated except for a link to this thread. [EDIT: I went ahead and added some items from this thread to the wiki.]

[Zoltan A. Kocsis (Z.A.K.)]

I’d like to propose two points I/we could write a few paragraphs about in the upcoming article on the project, provided others agree they're worth including.

1.

The majority of counterexamples were discovered using automated tools like SMT solvers, ATP, and similar (I think the largest of the 740 currently in All4x4Tables are from the brute force enumerator, then Mace4, then Vampire). Not only that, but a large number of the crucial implication proofs were also handled through ATP!

Had this project started years earlier, when first-order ATP tools weren't so good, I think we still would have filled in the implication table over time, perhaps even with more insight than the "deploy Vampire" approach. But the success of the ATP tools points to a Sutton-style "bitter lesson" for these sorts of universal algebra problems.

In the first days of the Equational Theories Project, there were many interesting suggestions for developing metatheory that would settle large batches of anti/implications uniformly (these should be gathered). But the automated tools worked so efficiently, the project's set aim was largely achieved way before these ideas could really bear their mathematical fruit! This even applies to the recent algebraic-geometric insights: if our search was just a tiny bit more effective, it might have been missed altogether, as the quadratics-based approach was swamped out by SMT-generated counterexamples initially!

Where does that leave us? I think developing tools (potentially AI-based tools) which extract useful mathematical insights from first-order proofs found by ATP proves would be valuable. Right now, we have a load of Vampire proofs, but we don't fully understand which ones hold valuable insights. Even if none are currently groundbreaking, I bet there are a few future Tricki entries hiding in there. This being mentioned in the article could set things up for grant proposals to do exactly that, or to get AI companies interested in insight mining.

2.

The second, related to the first, is a paragraph or two about semi-handmade counterexamples, as described in e.g. the 13x13 counterexample thread. I invested a fair bit of search-based, but ultimately manual effort in finding counterexamples, and I think I am not the only one. I think it's important to a.) document the type of human-machine teamwork mentioned in the linked thread while it still exists; b.) since in the spirit of the bitter lesson, automated tools could easily integrate these methods. Indeed, developing tools which have these strategies is something that should appear in ATP grant proposals shortly!

[Terence Tao]

These are great topics. I added a brief mention of each to the current plan of the paper.

[Shreyas Srinivas]

There were also some interesting implications discovered with the semi-automatic egg tactic. I would like to see how it compared with ATPs; Not in how many implications it solved but whether egg worked better on harder to find implications for ATPs. Another question to be addressed is, how did the authors choose the intermediate steps of the egg tactic if they did so. How much of it was "human-insight" driven?

[Zoltan A. Kocsis (Z.A.K.)]

Good point @Shreyas Srinivas - in fact, regardless of whether they outperformed classical ATPs, E-Graphs are certainly one of the big winners for me here, and they now definitely made it to my personal "pay attention" list!

[Terence Tao]

Perhaps when the implication graph is complete we can generate a standard test bench of implication problems that we can then test all of our automated methods (and some of our semi-automated ones) in an apples-to-apples comparison, as opposed to "who can implement their approach the fastest and snag the most unresolved implications?"

[Terence Tao]

Though I still don't quite see how to evaluate the difficulty of a given implication, other than to test a few standard automated theorem provers on it.

[Shreyas Srinivas]

Full disclosure, I am looking at certain model checking problems where I think certain semi automatic methods feel justified in principle. So I am curious to know how they work in practice.

[Shreyas Srinivas]

I think we could measure difficulty in many ways. For example: how many steps would it take for a random walk from the source equation to reach the entailed equation.

[Shreyas Srinivas]

In expectation of course

[Shreyas Srinivas]

More systematically, how many non-greedy rewrites have to be applied to reach the target from the source in the implication graph. How large are these rewrites

[Shreyas Srinivas]

But this is something to ask @Andrés Goens

[Will Sawin]

Terence Tao said:

Though I still don't quite see how to evaluate the difficulty of a given implication, other than to test a few standard automated theorem provers on it.

Since it's fine if a benchmark has some easy problems on it but bad if it misses an entire class of hard problems, it probably makes sense to come up with several different ways to measure difficulty and take N of the most difficult problems according to each for some reasonable N.

[Will Sawin]

"Length of the Lean proof in the final version" is one possible difficulty metric, or "Time to compile the Lean proof", maybe.

[Andrés Goens]

Shreyas Srinivas said:

More systematically, how many non-greedy rewrites have to be applied to reach the target from the source in the implication graph. How large are these rewrites

hmm, that's an interesting thought, although shortening an exitsing proof is already an NP hard problem in general and not so easy to establish the ground truth (see e.g. https://ieeexplore.ieee.org/abstract/document/10026585) i.e. the actual minimum.

[Andrés Goens]

but we could just take "the shortest chain of rewrites found by any method" in this project as a proxy, which coincidentally should be similar to the length of the lean proof in the final version (although there for example things like our tactic do a bit worse because they are less specialized and have some "boilerplate" conversions)

[Andrés Goens]

In general I think the difficulty of equational reasoning like this is usually when you have multiple options to rewrite, which by the restrictions of this project is very limited (you can have multiple matches on one term, but not multiple equations to choose from).

So, a lot of the interesting stuff happens when you have multiple laws (unsurprisingly). For example, assocativity + commutativity make things very hard, but I believe are still decidable in the ground theory, whereas adding distributivity makes it undecidable (that's with two symbols though). But then if you add a few more rules and get commutative rings, you get a decidable theory again (see the ring tactic). And of course you can state a lot of problems in algebra this way, as most algebraic structures are just sets of laws over magmas like this (I guess understandably the term "universal algebra")

[Andrés Goens]

I guess what I mean by that is that I have the impression that we had a domain where ATPs are especially good, and human ingenuity has been less necessary for that. (Maybe this is just copium and I still have to learn/internalize the bitter lesson that @Zoltan A. Kocsis (Z.A.K.) linked here though)

[Daniel Weber]

It might be interesting to explore magma properties that aren't laws, like cancellability

[Terence Tao]

And also to systematically study confluence

[Terence Tao]

Recording here an (anonymous) suggestion from my blog:

Let E denote the poset of magma equations with up to 4 operations, ordered by implication. By casting the equations to magmas with a unit element, one obtains a quotient poset E’ (there are more implications: e.g. x(xy)=xy implies xx=x when the magma has a unit element, but not in general). Further casting the equations to loops (magmas with unit where all left- and right- multiplications are invertible) will project the poset E’ further, say to E” (e.g. from x(yx)=x(xy) we immediately get yx=xy).

I will not try to advocate here that loops are “more interesting” than magmas. But from the point of view of a human being having to digest a computational project of this magnitude, E” would be more appealing and more manageable than E.

The sub-poset of E” consisting of ordered homogeneous equations of degree 1+1+2 (three operations), was determined in https://arxiv.org/abs/math/0701714. It would be quite nice if the current project will be able to determine the poset of ordered homogeneous loop equations of degree 1+2+2 or 1+1+3

[Trebor Huang]

How far would we be from determining the full structure of the lattice generated by these equations, once we deal with the two hypotheses implications? It would be very interesting to find out about implications with a large number of hypotheses that cannot be deduced from simpler implications!

[Andrés Goens]

Terence Tao said:

Recording here an (anonymous) suggestion from my blog:

Let E denote the poset of magma equations with up to 4 operations, ordered by implication. By casting the equations to magmas with a unit element, one obtains a quotient poset E’ (there are more implications: e.g. x(xy)=xy implies xx=x when the magma has a unit element, but not in general). Further casting the equations to loops (magmas with unit where all left- and right- multiplications are invertible) will project the poset E’ further, say to E” (e.g. from x(yx)=x(xy) we immediately get yx=xy).

I will not try to advocate here that loops are “more interesting” than magmas. But from the point of view of a human being having to digest a computational project of this magnitude, E” would be more appealing and more manageable than E.

The sub-poset of E” consisting of ordered homogeneous equations of degree 1+1+2 (three operations), was determined in https://arxiv.org/abs/math/0701714. It would be quite nice if the current project will be able to determine the poset of ordered homogeneous loop equations of degree 1+2+2 or 1+1+3

Isn't a magma with a unit element just a magma with an additional law (now with constants) though? So this would be a special case of looking at two laws (with constants), right?

[Terence Tao]

Trebor Huang said:

How far would we be from determining the full structure of the lattice generated by these equations, once we deal with the two hypotheses implications? It would be very interesting to find out about implications with a large number of hypotheses that cannot be deduced from simpler implications!

There is some prior discussion about the feasibility of at least determining the pair implications EquationX ∧ EquationY → EquationZ at #Equational > Search space for (EqX ∧ EqY) → EqZ. It looks borderline feasible, but scaling further may be difficult.

[Terence Tao]

Andrés Goens said:

Isn't a magma with a unit element just a magma with an additional law (now with constants) though? So this would be a special case of looking at two laws (with constants), right?

Yes, it is basically of the same framework as our current project. One could imagine several forks of this project in the future where other magma-like theories are studied. Our existing implication graph could be somewhat useful in any other project of this type, as it instantly lists all the short laws one can deduce from any single short law in their axiom set (provided that law involves only one binary operation), although presumably most of the interesting consequences come from combinations of multiple laws and/or multiple operations, so there would still be a lot of work to do.

[Terence Tao]

On another thread, @Alex Meiburg proposes studying the question of when a given law EquationX induces a law EquationY for a different operation that can be defined in some first-order logic sense from the original law. For instance, equation 543, which encodes subtraction in an abelian group, is not directly commutative or associative, but can be used to define an addition operation which satisfies both axioms.

[Will Sawin]

Terence Tao said:

On another thread, Alex Meiburg proposes studying the question of when a given law EquationX induces a law EquationY for a different operation that can be defined in some first-order logic sense from the original law. For instance, equation 543, which encodes subtraction in an abelian group, is not directly commutative or associative, but can be used to define an addition operation which satisfies both axioms.

Every law can be used to define xy=x and xy=y, which are associative but usually not commutative. The subtraction example has a further property that from an addition operation derived from a subtraction operation we can first-order define the original subtraction operation, which these examples do not share. It might be more interesting, but probably harder, to study operations defining other operations with this stronger property.

[Alex Meiburg]

Good catch. I think that's a better relationship to look at.

[Terence Tao]

Proposed by @Alex Meiburg : find explicit descriptions for the free magma for each of the 4694 laws.

[Andy Jiang]

Can we propose questions which are much less broad in scope (maybe this is wrong place)? I'm still curious whether all finite examples of 1485 are of size 2*n^2. I believe we still don't know why this is true.

[Terence Tao]

Sure, any mathematical question that can plausibly build off of this project is fair game here.

[Bruno Le Floch]

Andy Jiang said:

Can we propose questions which are much less broad in scope (maybe this is wrong place)? I'm still curious whether all finite examples of 1485 are of size 2*n^2. I believe we still don't know why this is true.

The "correct" conjecture is actually $n^2$ or $2n^2$ since we have examples of any of these orders, unless you want to exclude those that satisfy a stronger condition $(x\diamond y)\diamond(y\diamond z)=y$. Sorry, I didn't track the correct terminology there, maybe normal central groupoid?

[Andy Jiang]

You're right i forgot about those

[Michael Bucko]

A couple of ideas:

1. Create a competition like in ARC-AGI with the goal of proving all theorems with AI + ATP. We'd try to provide AIs with tools and techniques that would enable them to prove the theorems they haven't been able to solve so far.

2. Create a unified math platform. The go to market could be: Zulip with math AI agents + ATPs integrated + colab. See: https://buildermath.substack.com/p/on-math-platform

3. A project aiming at dealing with those emerging sporadic triplets. One approach to this could be creating a tool to deal with exceptional cases that cannot be systematically reduced or generalized.

4. Counterexample machine. Problems in, counterexamples out. As an API, dynamic library, or something that'd enable efficient integrations.

5. Infrastructure for such projects. Like W&B, but for math research projects. Related to 2.

6. Next-gen gradient descent for higher-order concepts (multi-layer).

7. A fine-tune of a foundational language model using datasets generated with the project (some models will require chat-formatted data).

8. Deeper AI integrations for proof generation.

9. Also related to 2. Tool for transforming math insight into code. A bit like Bootstrap for proofs. Perhaps a pip package. Have a look here: https://colab.research.google.com/drive/17ZJSD31HIfOsQJnDD0qA3XwVGw3xcuiy#scrollTo=e_wYXrTCxgMw (I made this using a colab from @Philip Zucker )

10. Parallel computing CLI on top of ATP scripts.

11. A diffusion model that generates new formalized mathematical knowledge.

12. Next-generation equation search with RL.

13. Interface / UX for theorem proving.

14. A proof optimization and eval tool. One would give it a Lean proof and it'd try to clean it up.

15. I was also thinking of running quantum experiments with q# - https://github.com/riccitensor/quantummath

16. Mathematical intuition model. Something that'd be trained on top blogs and insights, and then provide deeper insights & recommendations. Could be part of the fine-tune, i.e. related to 7.

17. Next-gen mathematical dataset, i.e. different data points could have different representations. Something like OEIS for proofs, techniques, etc. The good news is that one data point could have many representations in the embedding space.

18. Something like Mathematica for paper writing? It'd most likely feel like Colab with ATPs and agents doing part of the work.

19. Conjecture generation machine and network. Would require deep insights, specialized knowledge, function calling. I guess it'd send the conjectures for human peer review. It'd be also given some sort of eval.

20. A Python math pipeline library. One could specify [Duper: 1,000,000, z3: param1, param2, minizinc: param1, param2, Vampire: etc., Claude: prompt1, etc. ] in a config file, and then get well documented results (and the code). With a linter and tests. Doesn't pass the test? Do it again.

[Michael Bucko]

(deleted)

[Bruno Le Floch]

Another future direction: for which equations is there an interesting theory of smooth magmas satisfying this equation, and in particular some algebraic structure (possibly -oid) on the tangent spaces? For an entry point to some literature see the mathoverflow question "Lie groups vs Lie monoids", where people point to tangent spaces of Moufang loops being Malcev algebras.

[Terence Tao]

I think the use of smooth magmas is a possible new technique for the outstanding implications, I will experiment with that later today and see if it is at all fruitful.

[Bruno Le Floch]

Another future direction: for each equation, consider the category of magmas subject to this equation, and of magma morphisms between them; what properties does this category have? Is it closed under product/coproduct; what are its injective/projective objects, etc. For instance, magmas obeying the Tarski axiom (defining abelian groups equipped with subtraction) form an abelian category.

[Zoltan A. Kocsis (Z.A.K.)]

@Bruno Le Floch : This is, in some sense, a problem concerning properties of single equations instead of relationships between pairs of equations. Since that is the focus of classical universal algebra, one could call it better-understood than what we were/are doing in this project. Some general results: the category of all magmas which satisfy a given fixed equation is always closed under products by the HSP theorem - and in fact the category has all small limits and colimits. Looks like Day had some general results about injectivity. That's not to say it's not worth investigating on a large scale, of course.

[Matthew Bolan]

It is becoming somewhat clear (for example in all of the recent greedy algorithm advances) that understanding what statements of the form $\exists x_1,...,x_i f(x_1,...,x_i) = g(x_1,...,x_i)$ a given equation implies is important.

[Jose Brox]

Bruno Le Floch ha dicho:

Another future direction: for each equation, consider the category of magmas subject to this equation, and of magma morphisms between them; what properties does this category have?

One could also say that the categorical study of universal algebra is covered by Lawvere theory, and by monads more in general.

[Jose Brox]

Future direction: Implement an ATP specific for magmas which incorporates all the techniques developed in the project. Specifically, it should be able to:
1) Look for infinite countermodels by several constructions: linear models, translation-invariant models, Kisielewicz models, greedy models. I don't really know how automatable the greedy method is, but we could try to find heuristics, and @Matthew Bolan seems to have automatized the search for seeds.
2) Look for Austin equivalence, i.e., equivalence over finite models, by playing with injectivity and surjectivity, both by mathematical analysis and by imposing restrictions over the relevant maps (depending on the studied identity). I think this can all be automated, and @Vlad Tsyrklevich already has some code.
3) Look for immunities and apply this knowledge in its advantage (either to prove the implication or when looking for countermodels).
4) Make loops trying different search parameters for the same identity, in a smart way.
5) Show that a difficult identity is equivalent to several simpler ones, and try to show those instead.
6) [Anything else I'm forgetting]

This could be a metatool that called Vampire, Mace4, Prover9, etc. as subroutines to do the heavy lifting, and just implemented the new features. Perhaps @Michael Bucko could help in its development.

Oh, how I'd like to have this tool for the Higman-Neumann study :big_smile:

[Amir Livne Bar-on]

Thinking about finite implications, do we know that this problem is in the same computational class as general implications? (I haven't seen an argument for Turing-completeness of the latter problem, but it probably is)

[Terence Tao]

Well, it is in a different decidability class at least. The implication problem for laws on arbitrary magmas is known to be undecidable, but is semidecidable: if an implication is true for arbitrary magmas, then by the Birkhoff completeness theorem there is a finite proof, so one can run an algorithm that halts iff the implication is true. In particular the complement cannot be semidecidiable.

On the other hand, an implication for finite magmas has semidecidable complement: by brute force searching over all finite magmas, one can run an algorithm that halts iff the finite implication is false. So this must have a different decidability class than the general problem. (But I expect it would also be undecidable.)

[Douglas McNeil]

Quantify the "flexibility" of magmas, for some reasonable definition(s) of flexibility. For example, in the limit, x=x magmas are completely flexible at any order: you can change any from 0 to n^2 elements and still have a satisfying magma. Magmas with only one example at a given order are the least flexible, etc. Then there's extensional flexibility (how a magma behaves when adding a new element). It feels like there's a range of qualitatively different behaviour here, but this could be a false impression generated as an artefact of the techniques we're throwing at them.

This may have relevance to understanding why some equations have magmas which are far easier to work with using the numerical approaches than others.

[Ibrahim Tencer]

Further investigation of cardinality properties: are there models for every finite cardinality, and if not then which? And the same question for "simple" models i.e. those that are not a nontrivial product of two other ones. And the same questions for counterexample models, plus finding the smallest counterexample.

[Bruno Le Floch]

The notion of "simple" is made more complicated by flexibility: if a magma is obtained by taking a product of two magmas, then changing some unimportant entries of the multiplication table, then it may be bad to call it simple.

[Ibrahim Tencer]

Sure, that could be a further question too.

[Jose Brox]

Ibrahim Tencer ha dicho:

are there models for every finite cardinality, and if not then which?

In which context is this question asked, what are the restrictions (operations, elements, identities...)? I assume that you don't want to allow the identity $x = x$ nor the trivial models of any size in which $x*y=0$, but if we allow the commutativity law, then we can fill half the multiplication table however we like for any size, then get the other half by commutativity. The same happens with other laws that don't impose restrictions over the full multiplication table, like $x*x = x$, which only restricts the diagonal.

[Ibrahim Tencer]

Jose Brox said:

Ibrahim Tencer ha dicho:

are there models for every finite cardinality, and if not then which?

In which context is this question asked, what are the restrictions (operations, elements, identities...)? I assume that you don't want to allow the identity $x = x$ nor the trivial models of any size in which $x*y=0$, but if we allow the commutativity law, then we can fill half the multiplication table however we like for any size, then get the other half by commutativity. The same happens with other laws that don't impose restrictions over the full multiplication table, like $x*x = x$, which only restricts the diagonal.

I was just thinking about asking it for each individual equation that was part of the project. Obviously many cases will be trivial: if an equation has an operation on either side then it will be implied by the constant law and therefore allow a model of any size. And if it's of the form "x = W" with the right or left-most variable x then it will be implied by one of the absorptive laws and also have a model of any size. But, these models are only simple (or "product-simple" if you prefer) for prime cardinalities.

As mentioned above, 1485 is a less trivial case.

[Douglas McNeil]

Right now I'd really like to know more about which orders have 677 models.. unless there are lots of models around, mutation methods aren't very helpful, and when you only have a handful in total, there's not much to do. :sweat_smile:
Still, seems kind of fitting that the last unhandled case will probably involve some actual thinking and not just number-crunching!

[Jose Brox]

Ibrahim Tencer ha dicho:

And the same question for "simple" models i.e. those that are not a nontrivial product of two other ones

I think the usual names for this property are "directly irreducible" or "directly indecomposable".

[Douglas McNeil]

Even if we don't need something as fancy as lmfdb, maybe just factordb, I think it'd be good to have a place to store interesting magma we come across (finite easiest, of course.) Right now hard-to-find magma which might not be directly used in a refutation might be at risk of being lost to the sands of time, e.g. this recent 677 magma.

[Vlad Tsyrklevich]

Yes, one thing I'd like to eventually do is also add all of the magmas I found that satisfied some order 5 magma to the repository, and I hope @Jose Brox has kept his H-N refuting magmas around as those would also be good to keep. Maybe data/interesting_magmas/? Or maybe bonus_magmas/? That puts them separate from the rest of the magmas in All4x4Tables but I'm not sure that's such a big deal.

[Terence Tao]

One could imagine an upgrade to Finite Magma Explorer in which one can load magmas stored (in some plain text format) in some directory of the repository (maybe indexed by some hash of the magma, and supplied with an optional commentary<hash>.md file similar to how EquationExplorer functions to briefly explain the significance of the magma), and also one has the ability to "export" a given magma (with some user-supplied text for the commentary) into such a plain text format (with the hash provided), which can then be PR'ed to the repository later.

[Zoltan A. Kocsis (Z.A.K.)]

Speaking of: coming up with good isomorphism-invariant hash for magmas. Of course, such a hash cannot be both very good and easy to compute (even just group isomorphism is thought to be hard in the sense of complexity theory).

Solving this problem is overkill for the proposed Finite Magma Explorer enhancement, though: instead of hashing the magma, one can

1. hash the list of equations satisfied by the magma,
2. check if there's any commentary for the given hash,
3. if there is such commentary, solve magma isomorphism to check that the required commentary applies to the current magma.

The only expensive (and hard-to-implement) step here is 3, which is not strictly necessary, and not even strictly desirable. So this feature should not be hard to implement.

[Douglas McNeil]

I'm not sure I followed #1, but maybe I figured it out. At first I didn't see how it could work, because there are nonisomorphic magmas which satisfy the same set of equations (in our set, anyhow). That hash would be useful in the sense of building a hashmap, i.e. putting similar magmas in the same group, but not so good for choosing a filename because of collisions.

But maybe you had in mind a filename like <hash>_<arbitrary_incrementing_number>, and the idea was simply to cut down the number of candidates we'd need to do isomorphism checks against.

[Zoltan A. Kocsis (Z.A.K.)]

But maybe you had in mind a filename like <hash>_<arbitrary_incrementing_number>, and the idea was simply to cut down the number of candidates we'd need to do isomorphism checks against.

Yes, that's all we could hope for from a hash: it's a number with fixed size, and there are infinitely many magmas on finite carrier sets, so there will always be nonisomorphic magmas sharing the same number. The goal is to have one that's easy to compute, isomorphism-invariant, but lets us tell apart magmas with commentary from magmas without.

One could make much finer distinctions, e.g. by hashing the number of satisfying tuples for each equation instead of just the list of satisfied equations. But that's already much much slower to compute, especially for magmas with order 20 and above.

[Alex Meiburg]

There are some other cheap isomorphism tactics. The squaring map is a function M -> M. It produces a collection of rooted trees to describe all its data, and isomorphism testing of rooted trees is easy. So it's easy to at least distinguish magmas that have inequivalent squaring maps.

[Douglas McNeil]

:nod: So yeah, you meant hash in the dict mode ("we know there are going to be some collisions in practice, but we can handle that") as opposed to a hash in the md5ish one ("no real need to worry about a collision, the sun is likelier to explode").

[Zoltan A. Kocsis (Z.A.K.)]

@Douglas McNeil Afraid so. It'd be good to have a solution that doesn't produce collisions in practice, but I don't know how to do that (it's an interesting technical challenge for sure, which is why I discussed it in future work; I think finding one which works well over special cases, say small monoids, might already be hard for complexity-theoretic reasons).

[Terence Tao]

Perhaps working out the number of satisfying tuples for say a dozen one and two variable equations might be enough information to separate magmas in practice.

[Terence Tao]

Bruno Le Floch said:

Another future direction: for which equations is there an interesting theory of smooth magmas satisfying this equation, and in particular some algebraic structure (possibly -oid) on the tangent spaces?

Somewhat out of desperation due to the slow progress on 677 -> 255, I returned to this idea. I think smooth magmas are tied to two of the constructions we are already considering, namely piecewise linear extensions and cohomological extensions.

First suppose that we have a smooth magma with an idempotent element $0 \diamond 0 = 0$. For sake of notation I will assume the magma is one-dimensional and parameterized by the real line, although the general case is similar. Then we have a Taylor expansion
$x \diamond y = \alpha x + \beta y + a x^2 + bxy + cy^2 + \dots$
for small $x,y$, where the $\dots$ are cubic and higher terms and $\alpha,\beta,a,b,c$ are constants. Replacing $x,y$ by $\varepsilon x, \varepsilon y$ for some small $\varepsilon$ and using $(x,s)$ as shorthand for any quantity of the form $\varepsilon x + \varepsilon^2 s + O(\varepsilon^3)$ we see that
$(x,s) \diamond (y,t) = (\alpha x + \beta y, \alpha s + \beta t + a x^2 + bxy + cy^2)$
and so we see that this smooth magma induces a cohomological magma with a linear base and quadratic cocycle, which will obey all the laws that the original magma does. By Taylor expanding to higher order one obtains a tower of cohomological extensions, with the cocycles being polynomials of increasingly high degrees. If the magma is not just smooth, but analytic and connected, then any law that is satisfied by all levels of this tower will also be satisfied by the original magma thanks to analytic continuation. So the connected analytic magma is effectively an "inverse limit" of this tower.

If there are no idempotents, then the smooth magma operation on $M$ induces a magma on the tangent
bundle $TM$ which is basically a piecewise linear extension of $M$ that obeys exactly the same laws that $M$ does (note that $M$ is a submagma of $TM$). Further Taylor expansion gives further extensions into jet spaces that are of a "piecewise cohomological" flavor.

So basically smooth magmas are like special types of cohomological or piecewise linear magmas. They could theoretically be useful constructions (the compatibility conditions required to construct them are algebraic in nature and could for instance be worked out by Grobner basis type methods). By working over finite fields instead of the reals one could probably create finite analogues for at least the Taylor approximants to these magmas; but for the specific problem of resolving 677->255 for finite magmas, the implication is immune to these sorts of extensions, and so these magmas might only be useful as a new type of base model.

[Bruno Le Floch]

It's very nice that cohomological extensions show up in this picture! I think the discussion is still missing a piece that makes Lie algebras distinct from group cohomology: taking a commutator $ghg^{-1}h^{-1}$ to eliminate the linear part and focus on the quadratic part of the Taylor series. The analogue of that is that if all linear models of a given law (say, the Higman-Neumann law 42323216 characterizing groups) obey another law (say, the Tarski law 543 characterizing abelian groups), then evaluating the latter law for small variables $(x,s),(y,t),\dots$ will give $\text{LHS}=(z,u)$ and $\text{RHS}=(z,u+v)$ which may well differ in the quadratic terms. The difference $(0,v)$ only depends on the leading terms $x,y,\dots$ and not on $s,t,\dots$. It defines a notion of bracket $T_0M\times T_0M\times\dots\to T_0M$.

EDIT: This bracket does not exactly require an idempotent, it's enough to have a solution $a,b,\dots$ of the latter law, and we get a bracket taking tangent vectors at $a,b,\dots$ and producing a tangent vector at some new point which is the result of applying the lhs or rhs of the law to $a,b,\dots$.

[Bruno Le Floch]

You might be dismissing too quickly this way of constructing 677->255 counterexamples. Lie groups are a good way of constructing examples of nonabelian groups. If I understand correctly, some of their finite-field analogues (like $PSL(n,p)$ for most $n,p$) are non-abelian groups that are simple, hence cannot be written as a cohomological extension of an abelian group. By analogy, we might find some 677 magmas analogous to PSL matrix groups, and I don't see why they would obey 255.