Outstanding equations, v1

Stream: Equational

[Terence Tao]

Just for fun, here is a summary of the outstanding equations, modulo duality. Small enough to now fit on one page!

Three-variable equations (total yield: 68 48):

• 1485 x = (y ◇ x) ◇ (x ◇ (z ◇ y)) (yield 38): the weak central groupoid equation, discussed here (L)(C)
• 854 x = x ◇ ((y ◇ z) ◇ (x ◇ z)) (yield 16 10) (L) . Partially analyzed by @Daniel Weber , requires formalization at equational#701 (f)
• 1117 x = y ◇ ((y ◇ (x ◇ z)) ◇ z) (yield 10) (F) analyzed by @Terence Tao; formalized by @Daniel Weber (l-nc)
• 1437 x = (x ◇ x) ◇ (y ◇ (z ◇ x)) (yield 4) analyzed by @Terence Tao; formalized by @Daniel Weber (a)

The "Hardy-Ramanujan cluster" (total yield: 20 6):

• 917 x = y ◇ ((y ◇ y) ◇ (x ◇ y)) (yield 8) "Hardy" (F) - analyzed by @Pace Nielsen, requires formalization at equational#660 (g)
• 1526 x = (y ◇ y) ◇ (y ◇ (x ◇ y)) (yield 6) (F) analyzed by @Pace Nielsen ; requires formalization at equational#663 (g)
• 1729 x = (y ◇ y) ◇ ((y ◇ x) ◇ y) (yield 4) equational#665 "Ramanujan" (T) (L) (F) - claimed by @Shreyas Srinivas
• 1323 x = y ◇ (((y ◇ y) ◇ x) ◇ y) (yield 2) equational#667 (T) (L) (F) - claimed by @Bernhard Reinke
• 2541 "Littlewood" and 2744 are also in this cluster, but all outbound implications from these equations are conjecturally resolved (by confluence and a greedy algorithm, respectively).

Other two-variable equations (total yield: 38 2):

• 1722 x = (y ◇ y) ◇ ((x ◇ y) ◇ y) (yield 10) (S) - analyzed by @Pace Nielsen, requires formalization at equational#659 (g)
• 1518 x = (y ◇ y) ◇ (x ◇ (y ◇ x)) (yield 8) (S) analyzed by @Pace Nielsen , requires formalization at equational#661 (g)
• 3342 x ◇ y = y ◇ (x ◇ (x ◇ x)) (yield 8) (T) - analyzed by @Terence Tao , formalized by @Daniel Weber (a)
• 1516 x = (y ◇ y) ◇ (x ◇ (x ◇ y)) (yield 4 2) equational#664. One implication analyzed by @Pace Nielsen, requires formalization at equational#675 (g). Remaining implication is open. (L) (T) (F) (C)
• 3308 x ◇ y = x ◇ (x ◇ (y ◇ x)) (yield 4) - analyzed by @Pace Nielsen, requires formalization at equational#666 (g)
• 3352 x ◇ y = y ◇ (y ◇ (x ◇ x)) (yield 2) (L) analyzed by @Jose Brox and @Daniel Weber , requires formalization at equational#668 (f)
• 3475 x ◇ x = y ◇ ((x ◇ y) ◇ y)(yield 2) (L) (T) analyzed by @Douglas McNeil, requires formalization at equational#669 (f)

(T) - is known to be immune to a pure translation-invariant approach
(L) - is known to be immune to the linear magma approach
(F) - is known to be immune to finite model approaches
(S) - resists simple translation-invariant constructions on the integers
(C) - immune to commutative constructions
All remaining equations here have resisted ATPs, small finite models, the confluent approach, and the automatic greedy algorithm.

(a) - defeated by an ad hoc construction
(f) - defeated by a finite magma construction
(g) - defeated by a translation-invariant greedy construction
(l-nc) - defeated by a noncommutative linear construction

I would be cautiously optimistic that many of the outstanding two-variable equations will be amenable to either commutative or noncommutative translation-invariant approaches (although such approaches force the squaring map to be a bijection, which may potentially be a problem: note that squaring appears in every two-variable law except for 3308). The three-variable equations may require a different approach, however.

Some relations between the Hardy-Ramanujan cluster (via graphiti):

• It is open whether 1526 implies 1323. However, 1323 implies 1526. More graphiti
• It is open whether 917 ("Hardy") and 1729 ("Ramanujan") imply each other. More graphiti

[Terence Tao]

Would it make sense to turn each of the two-variable equations into tasks? The task would be to perform some now standard analysis on each one, e.g., testing the greedy translation-invariant method, and report back on the results. The point of using the task system is to avoid redundant effort where multiple people work on the same equation without coordination.

[Terence Tao]

3342 looks particularly feasible to analyze via the translation invariant approach, if anyone wants to give it a shot

[Pace Nielsen]

@Terence Tao I'll take 3308 and 1729.

[Bernhard Reinke]

I would take 1518

[Notification Bot]

6 messages were moved here from #Equational > Obelix: joining two approaches by Terence Tao.

[Shreyas Srinivas]

@Terence Tao : if these equations link to GitHub issues then managing claims will be easier

[Shreyas Srinivas]

I think these tasks are now becoming more like the byte sized ones that we had in the PFR project

[Terence Tao]

OK, I've created placeholder issues for each of the two-variable equations, though I couldn't find either @Pace Nielsen or @Bernhard Reinke on Github (and it's not clear that the output of the task is necessarily a PR) so I just added an "informal" claim in those cases. As it is only 11 equations I think I will be able to manage any synchronization issues between this thread and the github version manually; so people can either "claim" these equations here, or via github, as they prefer.

[Kevin Buzzard]

The mathlib maintainers have been talking about encouraging Zulip users who have github accounts to put their github userids in their Zulip profile -- there is an explicit field for this, and perhaps we've just seen a reason why this might be helpful. Please feel free to do this if you're happy to do so!

I'm not sure I remember any PFR projects which were as small as a byte! ;-)

[Kevin Buzzard]

It's absolutely great that you've got down from millions of equations to something which fits in a Zulip message by the way. I had no real feeling about the feasibility of this step at the beginning; I was pretty confident that the original graph of 16 or so equations would be nailed, but this is clearly several orders of magnitude harder.

[Shreyas Srinivas]

@Pace Nielsen and @Bernhard Reinke : Could you claim the respective equation tasks from the project dashboard? The contributions process is described in CONTRIBUTING.md

[Pace Nielsen]

I tried the translation invariant approach to 1729, and found the functional equation does imply the other functional equation (even allowing noncommutativity). So I'll retract my claim to that problem.

I've finished 3308 (proving the nonimplication using a fairly large starting seed).

Equation3308.tex
Equation3308.pdf

[Terence Tao]

I guess it's fitting that the equation with Ramanujan's number is unexpectedly tricky. I'll add commentary for this equation to reflect this, and upgrade equational#666 to a formalization task (and mark the conjecture).

[Terence Tao]

So this may partially affect 917 as well, due to the mutual open implication to 1729. Does 917 also have the same functional equation as 2541?

[Shreyas Srinivas]

Terence Tao said:

I guess it's fitting that the equation with Ramanujan's number is unexpectedly tricky. I'll add commentary for this equation to reflect this, and upgrade equational#3308 to a formalization task (and mark the conjecture).

equational#666

[Terence Tao]

I'm tempted to call 917 and 1729 "Hardy" and "Ramanujan".

[Shreyas Srinivas]

There's the issue list:

1. equational#659
2. equational#660
3. equational#661
4. equational#662
5. equational#663
6. equational#664
7. equational#665
8. equational#666
9. equational#667
10. equational#668
11. equational#669

[Terence Tao]

Using left and right multiplication operations, "Ramanujan" (1729) is $L_{y^2} R_y L_y = I$, whereas "Hardy" (917) is $L_y L_{y^2} R_y = I$. So for instance for finite magmas, the laws must be equivalent by the usual injectivity/surjectivity analysis.

[Terence Tao]

So the problem is indeed that for translation invariant magmas, $y \mapsto y^2$ is forced to be surjective. Ramanujan implies surjectivity of $L_{y^2}$, hence surjectivity of $L_y$ in the translation invariant model; also Ramanujan implies $L_y L_{y^2} R_y L_y = L_y$, hence $L_y L_{y^2} R_y = I$ (Hardy) by the surjectivity of $L_y$.

Weirdly, I can't seem to reverse the argument and deduce that Hardy implies Ramanujan for translation invariant models. (Ramanujan tells us little about the surjectivity of $R_y$, which seems to be the main obstacle here.) So maybe Hardy is still tractable in this approach even if Ramanujan is not.

[Terence Tao]

Perhaps unsurprisingly, the other two-variable open implication from Hardy, Equation 2541, is $R_y L_y L_{y^2} = I$ (and I now dub it "Littlewood"). Graphiti The one "easy" implication (which apparently Vampire already found) is that Ramanujan implies Littlewood: if $L_{y^2} R_y L_y = I$, then $L_y$ is injective, hence $L_{y^2}$ is also injective; it is clearly also surjective, hence invertible, and so one can conjugate Ramanujan into Littlewood.

[Terence Tao]

There is a very similar triality between 1323 ($L_y R_y L_{y^2}=I$), 1526 ($L_{y^2} L_y R_y = I$), and 2744 ($R_y L_{y^2} L_y = I$). Graphiti. For instance, all three laws are equivalent on finite magmas. I am open to suggestions for names for this trio.

Strangely, 2744 is conjecturally solved! I am trying now to trace where we got this solution from.

[Terence Tao]

Ah, ok, 2744 is the dual of 883, for which @Daniel Weber 's automated greedy algorithm was able to find a construction (pending formalization). Interesting though that this algorithm doesn't work for any of the other five equations of this type.

[Terence Tao]

1323 implies 2744 for translation-invariant models by a similar argument to previous, and so 1323 has comparable difficulty with Ramanujan. Reorganizing the original post in this thread accordingly.

[Pace Nielsen]

I analyzed 1516 using translations. Its functional equation does imply the functional equation for 255. (Interestingly, in the noncommutative case, the proof took some extra work.) However, 1516 does not imply 1489. I need to do family stuff, but later tonight I'll type up the details.

[Pace Nielsen]

Okay, here is the proof that 1516 does not imply 1489. There is one minor thing that troubles me; the initial seed seemed too easy to construct. Maybe taking (1,1)\in f saved much of the pain. shrug

1516NotImplies1489.pdf
1516NotImplies1489.tex

[Pace Nielsen]

As mentioned above by @Terence Tao the equation 3342 was particularly easy to analyze under the translation paradigm. It turns out that the solutions to the functional equation can be described very simply: Writing things multiplicatively, they are exactly the functions where f^2(1)=1, and where f(a)=b iff f(a^{-1})=ba^{-1}. (So you can essentially define f arbitrarily, except up to how it behaves on inverses.) All of the functional equations for the equations possibly implied by 3342 are satisfied, so no-go here.

[Pace Nielsen]

I just notice that the final implication from 1728 was handled before the current list was posted. I'm interested to know how it was handled.

[Terence Tao]

1728 is dual to 1841, which was handled by a tree model in equational#639, see also https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/1841.20.3F.3D.3E.20203 .

Opened equational#675 to formalize 1516 !=>1489, and narrowed #664 to handle the remaining anti-implication 1516 !=>255.

[Terence Tao]

It's possible that @Zoltan A. Kocsis (Z.A.K.) 's "modified translation-invariant" strategy may help resolve some of the implications that we now know to be immune to the pure translation-invariant approach.

[Pace Nielsen]

I believe Hardy is now completely done (by the usual translation arguments). We are getting close to having tested all remaining equations for this method.

I'll be back Monday. So if I made calculational errors, or other questions arise in the meantime, just know that I'll get to it then! :-)

917.pdf
917.tex

[Terence Tao]

It turns out that 3342 is simple enough to be resolvable with an ad hoc construction. The main trick is to build an operation in which x ◇ (x ◇ x) is not surjective and not idempotent (one can check that the implications hold in these cases). The following construction works: take the carrier to be the polynomial ring ℤ[t], and define ◇ according to the rules

t^n P ◇ t^n P = t^n P ◇ t^{n+1} P = 2P

whenever P(0) ≠ 0 and n ≥ 0,

t^{n+m} P ◇ 2 t^n P = 2 t^n P ◇ t^{n+m+1} P = tP

whenever P(0) ≠ 0 and n, m ≥ 0, and P ◇ Q = 0 otherwise. This can be checked to obey 3342 (with P ◇ (P ◇ P) = tP for all P) but not any of the four currently open laws. I've just uploaded this construction to the blueprint at equational#677 .

[Terence Tao]

My experience with 3342 suggests that the other two outstanding equations 3352, 3475 which involve at least one magma operation on both sides, could potentially be resolved with an example in which the magma operation P ◇ Q is mostly zero.

[Terence Tao]

I will claim 3475 to try this approach

[Fan Zheng]

@Terence Tao Maybe a page can be set up to host the information here and linked from the project home page, to make it more visible?

[Shreyas Srinivas]

The blueprint is where we are recording technical info

[Eric Taucher]

Kevin Buzzard said:

put their github userids in their Zulip profile

Note for others: The way to update a Zulip profile is not started by clicking on the icon for ones Zulip profile but to click the gear icon then selecting Personal settings

image.png

[Daniel Weber]

Terence Tao said:

It turns out that 3342 is simple enough to be resolvable with an ad hoc construction. The main trick is to build an operation in which x ◇ (x ◇ x) is not surjective and not idempotent (one can check that the implications hold in these cases). The following construction works: take the carrier to be the polynomial ring ℤ[t], and define ◇ according to the rules

t^n P ◇ t^n P = t^n P ◇ t^{n+1} P = 2P

whenever P(0) ≠ 0 and n ≥ 0,

t^{n+m} P ◇ 2 t^n P = 2 t^n P ◇ t^{n+m+1} P = tP

whenever P(0) ≠ 0 and n, m ≥ 0, and P ◇ Q = 0 otherwise. This can be checked to obey 3342 (with P ◇ (P ◇ P) = tP for all P) but not any of the four currently open laws. I've just uploaded this construction to the blueprint at equational#677 .

I'm having some trouble with this - consider x = y = t^2. Then, if I'm not mistaken, t^2 ◇ t^2 = 2, t^2 ◇ 2 = t, t^2 ◇ t = 0, and the equality isn't satisfied. What am I missing?

[Terence Tao]

Oops, t^{n+m} P ◇ 2 t^n P = 2 t^n P ◇ t^{n+m+1} P should be t^{m+1} P, not tP, sorry! The construction is supposed to be designed so that P ◇ (P ◇ P) = tP for all P, and then the equation reads P ◇ Q = Q ◇ tP. I will update the blueprint accordingly.

[Daniel Weber]

I was able to simplify the construction to Option (ℕ × ℕ), equational#682

[Terence Tao]

This is a nice illustration of the contrast (that I learned from @Heather Macbeth 's paper) between what makes a proof easy for humans to read, and what makes a proof easy for machines to read. Option (ℕ × ℕ) is certainly a simpler object (both formally and mathematically) than ℤ[t], but human mathematicians have a lot of experience with polynomials, and so operations such as "multiply a polynomial by 2, after removing all factors of t" are intuitive, whereas analogous operations on Option (ℕ × ℕ)such as

match x with
| some (a, b) =>  (0, b + 1)
| _ => none

while much simpler formally, take a bit of getting used to for a human mathematician reader. (Here, the components a, b of Option (ℕ × ℕ) are an abstraction of the number of factors of t and 2 respectively appearing in the polynomial construction, when the polynomial is non-zero; the none option of Option (ℕ × ℕ) corresponds to the zero polynomial.) I agree though that the Option (ℕ × ℕ) construction is the "right" one for this argument, even though it would certainly not have been the one I would have discovered first.

[Terence Tao]

Recording some notes on 3475 to document my thought processes. My initial thought here was to set x^2 to be mostly constant, e.g., x^2 = 0 for non-zero x and 0^2 = 1, as a minimalist way to refute x^2 ◇ x^2 = x^2, however I encountered an obstruction in that the 3475 equation forces an implication x ◇ y = x → x^2 = y^2 (proof: x^2 = y ◇ ((x ◇ y) ◇ y) = y ◇ x, hence y^2 = x ◇ ((y ◇ x) ◇ x) = x ◇ (x^2 ◇ x) = x^2) which, under the above hypotheses, prevented me from setting 0 ◇ y = 0 for any y, which conflicts with wanting 0 = 1^2 = 0 ◇ ((0 ◇ 1) ◇ 0).

So I am now exploring a different model in which the squaring function is split evenly between two values rather than being mostly concentrated on one value. In this model, elements x are either "positive" or "negative", with x^2 = -1 for positive x and x^2 = +1 for negative x, and imposing the existence of a reflection symmetry x → -x that is a magma isomorphism to simplify the calculations. This is still work in progress.

[Terence Tao]

OK, it took a ridiculous amount of trial and error, but I now have a model for 3475 that contradicts its outstanding implication to 3342. equational#685. The carrier is ${\mathbb Z} \backslash 0$ and the rule is that $x \diamond y$ is equal to $2y$ when $x,y$ have opposite sign; $x \diamond 3x = \mathrm{sgn}(x)$; $x \diamond x, x \diamond 2x, x \diamond 5x = - \mathrm{sgn}(x)$; $2y \diamond y = 3y$; and $x \diamond y = 5y$ in all other cases. The main point is that $x \diamond x$ only remembers the sign of $x$, while $x \diamond y$ is mostly determined by $y$ and the sign of $x$, which gives the identity $x \diamond x = y \diamond ((x \diamond y) \diamond y)$ a shot at being true, while $x \diamond x = (x \diamond x) \diamond (x \diamond x)$ has a shot of being false. Everything else is based around fixing enough edge cases to make it all work.

[Terence Tao]

It's possible that 1518 models can be built by some variant of the 3475 construction, in which $y \diamond y$ depends only on the "sign" of $y$, and $y \diamond x$ primarily depends on $x$ and the sign of $y$. For instance, if $y \diamond y = \mathrm{sgn}(y)$, then the law simplifies to $x = +1 \diamond (x \diamond (y \diamond x))$ for positive $y$ and $x = -1 \diamond (x \diamond (y \diamond x))$ for negative $y$, which doesn't look too bad, though there may be compatibility conditions between this law and $y \diamond y = \mathrm{sgn}(y)$ that could cause minor headaches. Anyway, I'm happy to leave this for someone else to claim if they wish.

[Terence Tao]

It turns out 1437 has an easy and useful model, despite being three-variable, being an "extension" of the base model $i \diamond j = j+1$ on ${\mathbb Z}/3{\mathbb Z}$. The counterexample is $G = {\mathbb N} \times {\mathbb Z}/3{\mathbb Z}$ with $(a,i) \diamond (b,j)$ defined to equal $(a-1,j+1)$ if $i=j+2$ and $a>0$; $(b,j+1)$ if $i=j+2$ and $a=0$; and $(a+1,j+1)$ otherwise. Details in equational#688 (to go into the "ad hoc" portion of the blueprint). The main thing is to ensure that the squaring map is non-surjective; in this case it is $(a,j) \mapsto (a+1,j+1)$.

[Terence Tao]

1117 can be resolved by the noncommutative linear magma method. It suffices to refute 2441, x = (x ◇ ((x ◇ x) ◇ x)) ◇ x.

Let the carrier $G$ be the space of integer-valued sequences $(a_1,a_2,\dots)$ with the left shift $L(a_1,a_2,\dots) = (a_2,a_3,\dots)$ and right shift $R(a_1,a_2,\dots)=(0,a_1,a_2,\dots)$. Note that $LR = 1$ but $RL \neq 1$. We then take the magma operation $x \diamond y = Rx - Ly$. We compute

$y \diamond (x \diamond z) = Ry - L(Rx-Lz) = Ry + L^2 z - x.$

Iterating this, we obtain the law 1117:

$y \diamond ((y \diamond (x \diamond z)) \diamond z) = Ry +L^2 z - (Ry + L^2 z - x) = x.$

On the other hand, one can compute

$(x \diamond ((x \diamond x) \diamond x)) \diamond x = (R+RL-1) L x$

which is certainly not $x$ in general (e.g., it annihilates $x = (1,0,\dots)$. I've opened a task for this at equational#691.

[Workflow: using left and right multiplication operations, 1117 is asserting that $L_y R_z$ is idempotent, and the main difficulty is to construct an example where $R_z L_y$ is not idempotent (2538). This is not possible in a finite model by the usual injectivity <-> surjectivity arguments. This reminded me of the left and right shift operators, which are a staple pair of counterexamples in functional analysis, which led me to try the noncommutative linear magma method.)

[Daniel Weber]

For 3352 (x ◇ y = y ◇ (y ◇ (x ◇ x))), note that if $x \diamond x = y \diamond y$ then for all $z$, $x \diamond z = y \diamond z$. Also, if $x \diamond z = y \diamond z$ for all $z$ then $z \diamond x = z \diamond y$ for all $z$.
If I'm not mistaken, this means we can quotient on the relation recursively defined by $R(x, x)$ and if $R(x \diamond x, y \diamond y)$ then $R(x, y)$, and it'll still satisfy 3352, and won't change in whether it satisfies 4065 (x ◇ x = ((x ◇ x) ◇ x) ◇ x).
Therefore that we can assume that $x \diamond x$ is injective. For a finite magma this implies it's surjective, but that still doesn't seem to imply 4065
Using $Sx = x \diamond x$ and the usual $L_x, R_x$, the equation is $R_y = L_y^2 S$ (note that is an equality of functions)

[Pace Nielsen]

1526 fell to the standard translation techniques.

1526.pdf
1526.tex

[Pace Nielsen]

1722 also fell. I'll check 1518 later when I have some time.

1722.pdf
1722.tex

[Shreyas Srinivas]

Time permitting, I would like to make an attempt at 1729. I wonder if some computer science data structure might yield nice counter examples, although anything that is immune to countable models will probably not be cracked.

[Shreyas Srinivas]

I have already made the claim on the GitHub issue. This message here is just to be doubly sure nobody has taken it

[Jose Brox]

Daniel Weber ha dicho:

If I'm not mistaken, this means we can quotient on the relation recursively defined by R(x,x) and if R(x⋄x,y⋄y) then R(x,y), and it'll still satisfy 3352, and won't change in whether it satisfies 4065

Indeed, with 3352 together with the rule xx = yy implies x = y, Mace4 produces a counterexample to 4065 with 8 elements (attached).
Mace4 3352 square injectivity 4065 INPUT.txt
Mace4 3352 square injectivity 4065 OUTPUT.txt

[Daniel Weber]

Huh, I really didn't expect a finite counterexample, especially one that small (finite magma explorer link: https://teorth.github.io/equational_theories/fme/?magma=1%204%202%202%201%206%200%200%0A2%203%202%204%203%206%201%201%0A2%202%202%202%202%202%202%202%0A4%202%202%200%200%206%203%203%0A0%201%202%203%205%206%205%206%0A4%204%202%204%206%204%204%206%0A1%203%202%200%205%204%207%206%0A1%203%202%200%206%206%206%206 )

[Terence Tao]

Nice combination of theory and ATP! And we finally got to test the "Export" feature of the Finite Magma Explorer!

[Daniel Weber]

Giving Vampire a minute it can find it even without injectivity of squaring - I'll give it 10 minutes for each remaining implication which doesn't have (F)

[Daniel Weber]

Does anybody happen to have a list of the strongest equations each equation is not known to not imply, or suggestions for how to generate one? If it can't find a model for A ∧ ¬B and B -> C I don't think it could find a model for A ∧ ¬C

[Terence Tao]

Since there are just five equations left (!), we can do this by hand through Equation Explorer / Graphiti.

• 1516 (T): only 1516 -> 255 is open now.
• 1323 (T) (L) (F) : only 1323 -> 2744 is open.
• 1729 (Ramanujan) (F): open implication is to Hardy (917) and 817. 917 implies 817, so the Hardy implication is the stronger.
• 854: According to Graphiti, the open implications to 107, 413, 1045, 1055, 1248, 1251, 3316, 3925 are unrelated to each other.
• 1485 (weak central groupoids): this one is a bit complicated because it is equivalent to its dual and so one can simplify the list of 19 outstanding implications a little bit. Graphiti Modulo duality, the strongest implications are to 1483, and 152. (By the way, the graphiti graph is a bit misleading here, as it got confused by 1485 being equivalent to its dual; this means that 1485 => X is equivalent to 1485 => X^*, but one can't necessarily identify X and X^* because of this due to outbound implications.) never mind, the equations on Graphiti are in fact equivalent.

[Daniel Weber]

Thanks! I'll run it now

[Terence Tao]

Daniel Weber said:

Giving Vampire a minute it can find it even without injectivity of squaring - I'll give it 10 minutes for each remaining implication which doesn't have (F)

I'm curious how much the addition of the human insight that one can assume wlog that squaring is injective led to any speedup of the Vampire run. (Of course, half an hour of thought to save thirty seconds of Vampire compute isn't much of a direct win, but the principle of finding human-generated facts about a given equation to assist the ATP may be a good paradigm for these last few equations.

[Daniel Weber]

With the assumption of squaring being injective it finished in 0.2s

[Terence Tao]

OK so you are saying that the human saved Vampire 59.8s of thinking time? :rolling_on_the_floor_laughing:

[Pace Nielsen]

Here is 1518.

Equation1518.pdf
Equation1518.tex

[Daniel Weber]

Terence Tao said:

OK so you are saying that the human saved Vampire 59.8s of thinking time? :rolling_on_the_floor_laughing:

After tweaking some settings I managed to get it to around 20 seconds, so only 19.8s :smile:

[Terence Tao]

Well, it's still a 100x speedup, so from that perspective it actually is a very good illustration of human - automated tool collaboration.

I'm also seeing that was a good idea to list all the "immuities" that each equation was known to have. This seems to help a lot with "weapon selection", in particular to figure out that finite magmas were still an option here. (This feels weirdly like one of the computer games I used to play, with weak central groupoids (1485) seemingly emerging as the "final boss"...)

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

Terence Tao said:

Nice combination of theory and ATP! And we finally got to test the "Export" feature of the Finite Magma Explorer!

It's great, but this is actually the fourth time we test it! :) The first person to contribute a counterexample using the Finite Magma Explorer was @David Renshaw, IIRC.

[Terence Tao]

Are there links to past discussion for this? This would be nice to record, either in my personal log, or in the final paper.

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

I'm not sure where the discussion took place, but the PR is equational#430.

[Pace Nielsen]

I've checked that the remaining equations don't fall to the linear map x\diamond y \mapsto ax+by, with coefficients from a noncommutative ring.

[Daniel Weber]

Is it possible that $x \diamond y \mapsto axb + cxd$ could work?

[Terence Tao]

I believe that's still linear in the (additive) endomorphism ring of the original ring, so my guess is no

[Terence Tao]

wait, I withdraw the claim

[Terence Tao]

Maybe I reinstate it. You're asking for a law $x \diamond y = L_a R_b x + L_c R_d y$ where $L_a, R_b$ are the left and right multiplication operators in the ring $R$ (not the magma). This can be thought of as a quotient of the law $S \diamond T = L_a R_b S + L_c R_d T$ where $S, T$ now live in the endomorphism ring $End(R)$ of additive homomorphisms from $R$ to itself. This is now a noncommutative linear law in $End(R)$. If an anti-implication cannot be disproved here, I think it can't be disproved in the quotient model either

[Terence Tao]

(One may need R to be torsion free or something to actually get a quotient, but I think this is only a minor technical loophole that will be difficult to exploit.)

[Daniel Weber]

Daniel Weber said:

Thanks! I'll run it now

It found a counterexample to 854 -> 107,1248,1251 ( https://teorth.github.io/equational_theories/fme/?magma=%5B%5B5%2C%2011%2C%203%2C%205%2C%200%2C%200%2C%2011%2C%206%2C%200%2C%200%2C%2011%2C%206%5D%2C%0A%20%5B4%2C%202%2C%201%2C%204%2C%201%2C%201%2C%204%2C%201%2C%201%2C%201%2C%204%2C%201%5D%2C%0A%20%5B2%2C%202%2C%207%2C%202%2C%208%2C%204%2C%204%2C%202%2C%204%2C%208%2C%202%2C%208%5D%2C%0A%20%5B5%2C%2011%2C%203%2C%205%2C%203%2C%203%2C%2011%2C%201%2C%203%2C%203%2C%2011%2C%201%5D%2C%0A%20%5B4%2C%204%2C%207%2C%204%2C%207%2C%204%2C%204%2C%204%2C%204%2C%208%2C%204%2C%208%5D%2C%0A%20%5B5%2C%205%2C%207%2C%205%2C%205%2C%204%2C%204%2C%205%2C%2010%2C%205%2C%205%2C%205%5D%2C%0A%20%5B5%2C%205%2C%2010%2C%205%2C%206%2C%2010%2C%204%2C%206%2C%2010%2C%206%2C%205%2C%206%5D%2C%0A%20%5B9%2C%207%2C%207%2C%209%2C%207%2C%207%2C%207%2C%201%2C%207%2C%207%2C%207%2C%208%5D%2C%0A%20%5B8%2C%208%2C%207%2C%208%2C%208%2C%204%2C%204%2C%208%2C%2010%2C%208%2C%208%2C%208%5D%2C%0A%20%5B9%2C%209%2C%207%2C%209%2C%207%2C%209%2C%209%2C%209%2C%209%2C%208%2C%209%2C%208%5D%2C%0A%20%5B9%2C%204%2C%2010%2C%204%2C%2010%2C%2010%2C%209%2C%2010%2C%2010%2C%2010%2C%204%2C%2010%5D%2C%0A%20%5B9%2C%2011%2C%207%2C%209%2C%207%2C%2011%2C%2011%2C%209%2C%2011%2C%207%2C%2011%2C%208%5D%5D )

[Pace Nielsen]

(deleted)

[Terence Tao]

That's great! So 854 is partially resolved, though there are still five open implications. Perhaps as we analyze 854 further, we will find some theoretical insights that we can somehow combine with the brute force ATP method to get more examples, as was the case with 3352. It's interesting to see these older methods (finite magmas, (noncommutative) linear constructions) come back for one last hurrah!

[Terence Tao]

Roughly how long did it take Vampire to find that example? Was it fully automated, or partially human assisted?

[Daniel Weber]

It only took 15 seconds with 107 as the target, it was quite surprising it didn't find it previously (when the target is 1248 or 1251 it took ~90s). It's fully automatic

[Terence Tao]

Hopefully if we find a comparable human insight to the problem as with 3352 we can help vampire find more examples.

[Terence Tao]

It's actually rather surprising that 851 admits this order 12 example. Naively, the law imposes 12^3 conditions on a multiplication table with only 12^2 degrees of freedom, so there must be some secret structure somewhere. If we can figure out what additional properties this magma obeys, this may help guide the ATP to find more such examples like this.

[Terence Tao]

Certainly it looks quite far from being left-cancellative (many repetitions on each row), which makes sense actually after looking at the form of 851, as it reduces the role of the z parameter. Can we find some sort of viable ansatz in which the magma operation doesn't depend too strongly on the second argument?

[thormikkel]

(edit: mistaken)

[Terence Tao]

A question for @Pace Nielsen , while his memories are still fresh: for pedagogical purposes, which of the translation invariant greedy algorithm constructions would you recommend to put in the paper to illustrate the method with as few technicalities as possible? We could perhaps describe two instances of the construction, one with very few complications and one with some more complications.

[Pace Nielsen]

Terence Tao said:

A question for Pace Nielsen , while his memories are still fresh: for pedagogical purposes, which of the translation invariant greedy algorithm constructions would you recommend to put in the paper to illustrate the method with as few technicalities as possible? We could perhaps describe two instances of the construction, one with very few complications and one with some more complications.

The bifurcation tree argument need not appear unless you want to mention it (as all such instances can be subsumed by simpler arguments).

The argument for 1526 is fairly simple. I think of the 5 conditions there as follows.

(1) Finiteness of E is for simplicity. [It is not always necessary, but greatly simplifies case analysis.]
(2) Functionality of E is necessary for the full extension to be a function.
(4) This is the closure procedure necessary to guarantee that the functional equation holds at $a$.
(3) Starting with $a=1$ (or 0 if working additively), and using the closure procedure, one often sees some strange behaviors arise. These can be avoided in the general construction by just guaranteeing that $E$ has enough closure starting at 1. [This is most prevalent in the 3308 case, where a large initial seed was needed.]
(5) When proving the extension theorem, one naturally runs into certain issues that can arise when trying to extend generically. Conditions like (5) are added to prevent these bad issues from arising.

[Terence Tao]

Thinking out loud about 854: the order 12 example has $x \diamond y = x$ for large number of pairs $x,y$. This makes sense actually, given how 854 is an equation of the form $x = x \diamond (\dots)$. So one can rephrase the problem of building an 854 magma as follows: one needs to find a "reasonably large" subset $E$ of $G \times G$, set $x \diamond y = x$ for $(x,y) \in E$, and then figure out a way to fill in the rest of the multiplication table in such a way that
$(x, (y \diamond z) \diamond (x \diamond z)) \in E \quad (*)$
for all $x, y, z$. Note that there is a transitivity-type axiom: if $(y,z) \in E$ and $(x,z) \in E$, then $(x,y \diamond x) \in E$. In particular, if $(y,z), (x,z), (y,x) \in E$, then $(x,y) \in E$. Maybe one can make a guess what $E$ should be first (e.g., using the order 12 magma as inspiration) and then try to fill out the rest of the magma via an ATP? [One can take $E$ to be all of $G \times G$ to give a left absorptive magma, but then one doesn't rule out any implications.]

Related thought: even outside of $E$, it seems to make sense to have $x \diamond y$ take on very "few" values (as $y$ varies) somehow, in order to make it easier to obey conditions such as (*), in particular setting up some relationships between $y \diamond z$ and $x \diamond z$. I noticed that each row of the finite magma only takes on a small number of values, for instance. Not sure how to take this observation further, though.

[Terence Tao]

Wild guess: maybe make the axiom that $E$ is an equivalence relation? Or maybe just the reflexive axiom $x \diamond x = x$? Does this make it easier to find counterexamples?

[Terence Tao]

According to Finite Magma Explorer, the order 12 example of an 854 magma obeys a bunch of random laws (818, 854, 1031, 1225, 3867) in addition to the open implications and the known consequences. Perhaps one could impose one or more of these laws and see if (a) it makes it faster to regenerate the example, and (b) if it can produce more examples?

[Terence Tao]

An observation about the order 12 magma: it almost obeys the 10 law $x = x \diamond (y \diamond x)$, with the only exception being $0 \neq 0 \diamond (2 \diamond 0)$. Note that this law implies all the currently open implications.

It kind of makes sense that an 854 magma would obey this law quite often because it holds whenever there is at least one $z$ such that $y \diamond z = y$ and $x \diamond z = x$. Since 854 also suggests that the law should be left-absorptive a significant fraction of the time (as is the case in the order 12 example), we should then have 10 holding almost all the time.

Perhaps if we impose the rule that $x = x \diamond (y \diamond x)$ for all but precisely one exception (e.g., $(x,y) = (0,1)$ this would allow for faster generations of magma counterexamples?

[Pace Nielsen]

Along the lines of what Terry proposed, how difficult would it be to do the following?

For each i from 1 to 10,000 (so a bit past where we stopped enumerating equations), consider 854+Equation i, and see if Vampire can find a counter-example to one of the open implications?

If not unfeasible, one could keep a record of which indices $i$ didn't cause problems, and then iterate, adding a second new equation to the mix.

[Daniel Weber]

Terence Tao said:

An observation about the order 12 magma: it almost obeys the 10 law $x = x \diamond (y \diamond x)$, with the only exception being $0 \neq 0 \diamond (2 \diamond 0)$. Note that this law implies all the currently open implications.

It kind of makes sense that an 854 magma would obey this law quite often because it holds whenever there is at least one $z$ such that $y \diamond z = y$ and $x \diamond z = x$. Since 854 also suggests that the law should be left-absorptive a significant fraction of the time (as is the case in the order 12 example), we should then have 10 holding almost all the time.

Perhaps if we impose the rule that $x = x \diamond (y \diamond x)$ for all but precisely one exception (e.g., $(x,y) = (0,1)$ this would allow for faster generations of magma counterexamples?

This doesn't seem to make it faster.

Terence Tao said:

According to Finite Magma Explorer, the order 12 example of an 854 magma obeys a bunch of random laws (818, 854, 1031, 1225, 3867) in addition to the open implications and the known consequences. Perhaps one could impose one or more of these laws and see if (a) it makes it faster to regenerate the example, and (b) if it can produce more examples?

This doesn't seem to work either. It's a bit faster, but not significantly

Terence Tao said:

Wild guess: maybe make the axiom that $E$ is an equivalence relation? Or maybe just the reflexive axiom $x \diamond x = x$? Does this make it easier to find counterexamples?

The reflexive axiom implies all open implications from 854, even allowing for three exceptions

[Daniel Weber]

Pace Nielsen said:

Along the lines of what Terry proposed, how difficult would it be to do the following?

For each i from 1 to 10,000 (so a bit past where we stopped enumerating equations), consider 854+Equation i, and see if Vampire can find a counter-example to one of the open implications?

If not unfeasible, one could keep a record of which indices $i$ didn't cause problems, and then iterate, adding a second new equation to the mix.

Searching for counterexamples can take some time, but searching for sets of equations which don't quickly imply a given implication should be feasible, and a counterexample search could be run on those

[Daniel Weber]

Terence Tao said:

OK, it took a ridiculous amount of trial and error, but I now have a model for 3475 that contradicts its outstanding implication to 3342. equational#685. The carrier is ${\mathbb Z} \backslash 0$ and the rule is that $x \diamond y$ is equal to $2y$ when $x,y$ have opposite sign; $x \diamond 3x = \mathrm{sgn}(x)$; $x \diamond x, x \diamond 2x, x \diamond 5x = - \mathrm{sgn}(x)$; $2y \diamond y = 3y$; and $x \diamond y = 5y$ in all other cases. The main point is that $x \diamond x$ only remembers the sign of $x$, while $x \diamond y$ is mostly determined by $y$ and the sign of $x$, which gives the identity $x \diamond x = y \diamond ((x \diamond y) \diamond y)$ a shot at being true, while $x \diamond x = (x \diamond x) \diamond (x \diamond x)$ has a shot of being false. Everything else is based around fixing enough edge cases to make it all work.

I'm having some trouble formalizing this - setting $x = 1, y = 3$, we get $x \diamond y = 1, (x \diamond y) \diamond y = 1, y \diamond ((x \diamond y) \diamond y) = 5$, while $x \diamond x = -1$. What am I missing?

[Terence Tao]

Ugh, I had simply missed this case. I have to withdraw my proof here, so that 3475 is again open. :sad:

[Pace Nielsen]

I realized that there is another source of asymmetry in the translation-invariant technique. I've been consistently using the "left-favored" map $a\diamond b = f(ba^{-1})a$, which "keeps" the left factor. There is also a "right-favored" map (or, I believe equivalently, the left-favored map on the dual equation). I haven't tested the right-favored maps on the open implications. I'll try doing that tomorrow, if nobody gets to it before me.

By the way, with so few equations left, does it make sense anymore to claim equations? I'll hold off on trying the right-favored translations on the claimed equations until that's cleared up.

[Bernhard Reinke]

Hm, I am curious about your sign / ordering convention, I always used $a \diamond b = a f(a^{-1} b)$. The point is that this is left invariant with respect to group multiplication, we have $ga \diamond gb = ga f(a^{-1}b) = g (a \diamond b)$. If it is truly left invariant, then preferring the left or the right sight doesn't matter, we have $a \diamond b = a (1 \diamond a^{-1}b) = b (b^{-1}a \diamond 1),$ so we just could define $g(z) = z \diamond 1$ and get $a \diamond b = b g(b^{-1} a)$.

On the other hand, I don't think this works with the law $a \diamond b = f(b^{-1} a)a$. This is (for general non-commutative groups) neither left nor right invariant. Of course we can define magmas this way, but I am not sure you get the number of variable reductions as in the invariant cases.

Or is $a \diamond b = f(b^{-1} a) a$ a typo and you meant the right invariant $a \diamond b = f(b a^{-1}) a$?

[Pace Nielsen]

That was a typo (fixed now). [Edited to add: One can incorporate the inversion of $ba^{-1}$ into $f$, so actually the typo shouldn't have any relevance.]

[Pace Nielsen]

By the way, for added context, here is an easy example explaining how the asymmetry really can affect computations.

Consider the law $x=x\diamond y$. Taking $y=hx$ and using the translation-invariance $a\diamond b=f(ba^{-1})a$, we get the functional equation $f(h)=1$. [Or, using Bernhard Reinke's choices $y=xh$ and $a\diamond b=af(a^{-1}b)$ we get the same functional equation.)

On the other hand, using the same "left-favored" choices, but for the dual equation $x=y\diamond x$, we get the functional equation $f(h)=h$, the identity function.

[Terence Tao]

Just a note: on analyzing my error in proving 3475, there is an additional identity that magmas with this law obey that obstructed my approach, and will probably need to be taken into account in any other analysis. Writing $x^2 = x \diamond x$, $P(x) = x \diamond x^2$, we have the identity $P(x^2) = P(x)^2$. Proof: write the 3475 law as $x^2 = L_y R_y^2 x$. We have $x^2 = L_{x^2} R_{x^2}^2 x = L_{x^2} (P(x) \diamond x^2)$, hence $R_{P(x) \diamond x^2} x^2 = x^2$, then $(x^2)^2 = L_{P(x) \diamond x^2} R_{P(x) \diamond x^2}^2 x^2 = (P(x) \diamond x^2) \diamond x^2 = R_{x^2}^2 P(x)$, then $P(x)^2 = L_{x^2} R_{x^2}^2 P(x) = L_{x^2} (x^2)^2 = P(x^2)$.

[Terence Tao]

Pace Nielsen said:

I realized that there is another source of asymmetry in the translation-invariant technique. I've been consistently using the "left-favored" map $a\diamond b = f(ba^{-1})a$, which "keeps" the left factor. There is also a "right-favored" map (or, I believe equivalently, the left-favored map on the dual equation). I haven't tested the right-favored maps on the open implications. I'll try doing that tomorrow, if nobody gets to it before me.

I believe the right-favored maps are simply the left-favored maps for the opposite group (note one reverses the group operation, but doesn't reverse the magma operation), so they shouldn't rule out anything new. (Note that in the example you gave, $f(h)=1$ can rule out just as many equations as $f(h)=h$; for instance, they rule out each other.)

One observation is that the translation-invariant approach is basically restricting to magmas that have a transitive free action of isometries. One could possibly generalize this to magmas with just a transitive action of isometries, similar to how Cayley graphs can be generalized to Schreier graphs. This corresponds (using your left-favored notation, in which the symmetry acts on the right) to a carrier of the form $H \backslash G$ where $H$ is a subgroup (not necessarily normal) of a group $G$, and (using your left-favored notation) the law is of the form $Ha \diamond Hb = f(ba^{-1}) a$, where $f: G \to H \backslash G$ is a map that needs to obey the equivariance property $f(ah) = f(a)h$ to keep the operation well-defined. Potentially this construction is more general and could rule out more laws if one takes a non-normal $H$ (for normal $H$ this collapses to a translation-invariant construction on the quotient group $G/H$).

By the way, with so few equations left, does it make sense anymore to claim equations? I'll hold off on trying the right-favored translations on the claimed equations until that's cleared up.

Well, I think it's still better to avoid duplication of effort (or to give undue time pressure on what is, after all, a purely voluntary effort that is meant to be enjoyable). Now that I unclaimed 3475, perhaps you could try the translation-invariant approach there?

[Pace Nielsen]

The translation-invariant approach on 3475 doesn't work.

[Terence Tao]

OK, so 3475 is actually quite a challenging equation!

[Douglas McNeil]

Hmm:

https://teorth.github.io/equational_theories/fme/?magma=2%203%204%206%202%206%204%204%202%0A4%202%204%205%202%203%200%207%202%0A8%208%203%203%203%200%201%202%205%0A8%208%202%203%207%200%201%202%205%0A8%208%207%202%203%200%201%203%205%0A2%204%204%207%202%202%203%204%206%0A3%202%204%207%202%204%202%204%204%0A8%208%203%202%207%200%201%203%205%0A1%205%204%207%202%202%203%207%202

[Terence Tao]

Wow! How did you find this example?

[Terence Tao]

It's moot now, but here is a proof that my general construction (in which $x \diamond x = -\mathrm{sgn}(x)$) cannot work for 3475. Here, $L_1 R_1^2 (-1) = (-1)^2 \neq 1^2 = L_1 R_1^2 1$, hence $R_1 (-1) \neq R_1 1 = -1$. But $R_1(-1) = P(-1) = P(1)^2 = \pm 1$, hence $R_1(-1) = 1$. Similarly $R_{-1} 1 = -1$, hence $1 = (-1)^2 = L_1 R_1^2 (-1) = L_1 (-1) = R_{-1} 1 = -1$, contradiction.

[Douglas McNeil]

I'd like to say it was deep contemplation of the graph-theoretical implications, :wink: but really I used glucose via pysat. Imposed 3475 directly, and demanded (1,1) -> 2, which didn't help by itself, but adding (2,2) -> 3 did. Wasn't having any luck at low order but cranked up to 12, found one, and then found a lower-N one.

[Terence Tao]

There seems to be a surprising amount of power remaining in the ATP-powered finite magma approach, guided by adding suitable additional axioms. Three of the five equations outstanding are not known to be immune to finite counterexamples, so that gives some hope of more progress. (I see we just got a new tranche of order 8 examples for 1485 that hopefully gives some insight.)

[Terence Tao]

Technical note: I am temporarily commenting out two of the conjectures connected to prior finite magma examples. The reason for this is that Finite Magma Explorer no longer lists the instructions to upload a finite magma to All4x4Tables if it sees that the implication is already conjecturally proven. I will suspend the conjectures, grab the text from FME, put it into the relevant issues, then restore the conjectures. So you may see some backwards motion in the conjectural portion of the dashboard in the near term.

[Daniel Weber]

Perhaps it would be easier to just have FME ignore conjectures?

[Terence Tao]

Yeah, but this is a fix I can implement by myself (the main bottleneck is waiting for the CI), and with only five equations left, I don't expect this to be much of an issue going forward. I guess maybe one could eventually have an option in FME to ignore conjectures, but it wouldn't be a priority for me.

[Michael Bucko]

Douglas McNeil schrieb:

I'd like to say it was deep contemplation of the graph-theoretical implications, :wink: but really I used glucose via pysat.

Amazing! And thank you for mentioning the tool. Could you please share the code?

[Terence Tao]

OK, I see that @Douglas McNeil has uploaded a 3459 counterexample in equational#717 - thanks! (Though, strangely it didn't trigger any CI, so I don't know if it will actually propagate to be proven yet). I've disabled the conjectures for 854 and 3352, so there should be no difficult implementing equational#701 and equational#669 now. Should be a good test case to see if the instructions given in Finite Magma Explorer actually work!

(and I guess there is no point re-enabling these conjectures, since presumably once the above instructions are executed, these implications will be listed as formally proved.)

[Vlad Tsyrklevich]

The python script to generate the lean files needs to be run as well.

[Douglas McNeil]

Ah, sorry; couldn't find the script, although there it is in src, so assumed the instructions were outdated..

[Douglas McNeil]

By way of apology:

https://teorth.github.io/equational_theories/fme/?magma=7%207%207%204%207%205%207%204%0A4%206%205%201%201%205%207%206%0A4%207%201%202%202%205%205%201%0A4%206%201%204%204%205%202%204%0A7%206%201%204%203%205%202%200%0A5%205%205%205%205%205%205%205%0A4%205%207%206%206%205%202%202%0A4%201%202%204%200%205%206%200

[Pietro Monticone]

Douglas McNeil said:

Ah, sorry; couldn't find the script, although there it is in src, so assumed the instructions were outdated..

I'll update it in a few minutes.

[Douglas McNeil]

I submitted a one-line PR, FWIW.

[Vlad Tsyrklevich]

Douglas McNeil said:

I submitted a one-line PR, FWIW.

There's a missing file that needs to be git added

[Pietro Monticone]

Pietro Monticone said:

Douglas McNeil said:

Ah, sorry; couldn't find the script, although there it is in src, so assumed the instructions were outdated..

I'll update it in a few minutes.

Done. Here is the related commit.

[Terence Tao]

Two observations on 1516 x = (y ◇ y) ◇ (x ◇ (x ◇ y)), and its open implication to 255 x = ((x ◇ x) ◇ x) ◇ x:

1. Suppose we have a finite 1516 magma. We can write 1516 as $x = L_{y^2} (x \diamond (x \diamond y))$, so $L_{y^2}$ is surjective, hence invertible. On the other hand, the $x=y^2$ case of 1516 gives $y^2 = L_{y^2}^3 y$, hence $y = L_{y^2}^{-3} y^2$. So the squaring map $y \mapsto y^2$ is injective, hence is also invertible. Since all the $L_{y^2}$ were invertible, $L_y$ is invertible also. So perhaps one can help the search for finite solutions to 1516 by adding "squaring is invertible" and "left multiplication is invertible" as additional axioms.
2. One feature of (abelian) translation-invariant magmas is that the squaring map is a magma isomorphism (in fact every word map of one variable is a magma isomorphism). It is this fact that is blocking us from getting an anti-implication to 255 by abelian translation-invariant magmas. Indeed, we have $x^2 = (x^2 \diamond x)^2 \diamond (x^2 \diamond (x^2 \diamond (x^2 \diamond x)) = (x^2 \diamond x)^2 \diamond x^2$. If squaring is an isomorphism, this implies 255: $x = (x^2 \diamond x) \diamond x$. So perhaps one intermediate target is to find a 1516 counterexample the squaring homomorphism law $(x \diamond y)^2 = (x^2 \diamond y^2)$ (which, for finite 1516 magmas at least, is equivalent to squaring being an isomorphism, by part 1).

[Daniel Weber]

This shows that 1516->255 is true for finite magmas (proof by Vampire): using 1516, $x = y \diamond (x \diamond (x \diamond \sqrt y))$.
Now we have (*) $x = (x \diamond \sqrt x)^2 \diamond (x \diamond (x \diamond (x \diamond \sqrt x))) = (x \diamond \sqrt x)^2 \diamond x$. Now $(x \diamond \sqrt x)^2 = x^2 \diamond ((x \diamond \sqrt x)^2 \diamond ((x \diamond \sqrt x)^2 \diamond x))) = x^2 \diamond ((x \diamond \sqrt x)^2 \diamond x) = x^2 \diamond x$, and using that in (*) we get
$x = (x^2 \diamond x) \diamond x$, which is exactly 255

[Pace Nielsen]

Request: Could someone with access to Vampire (or another ATP) check if 1516 implies x = x ◇ (x ◇ (x ◇ ((x ◇ x) ◇ x)))?

[Daniel Weber]

It doesn't seem to

[Terence Tao]

Hmm, so 1516 (or more precisely 1516->255) is collecting a disturbing amount of immunities (in contrast to 1516=>1489, which we were able to dispatch). In particular the above analysis shows that 255 is already implied for square numbers. So for a counterexample we need an infinite, non-translation invariant, nonlinear example for which squaring is not surjective...

[Terence Tao]

I guess we could ask Vampire if 1516 plus commutativity implies 255, just to check off one more immunity

[Daniel Weber]

Terence Tao said:

I guess we could ask Vampire if 1516 plus commutativity implies 255, just to check off one more immunity

It does, yes

[Terence Tao]

/poll Should I create a new thread to focus on the four remaining equations besides 1485?
No, current "outstanding equations" thread is fine.
Yes, summarize previous progress and start a new thread.
Start one new thread for each of the other four equations, summarizing progress for each.

[Pace Nielsen]

@Daniel Weber Thank you for your quick response! A couple more questions.

Define the left powers recursively by x^{n+1} = x^n ◇ x. (So 255 is just x = x^4.) Does 1516 imply x = x^7?

Consider a sort of "flip-injectivity": a ◇ b = c ◇ d implies b ◇ a = d ◇ c. Does 1516 plus flip-injectivity imply 255?

[Daniel Weber]

It doesn't seem to imply x = x^7, and together with flip-injectivity it implies 255

[Pace Nielsen]

This is a long shot then. Does it imply x = x^n, for any "smallish" n?

[Pace Nielsen]

I really should just get access to Vampire myself, so I can try these things.

[Pace Nielsen]

Specifically, I'm thinking about n = 10, 13, 16, 19, 22.

[Terence Tao]

Based on polling, I will now create new threads for 1516 and 854. Until then, you can keep discussing here, and I will move coments accordingly. As for 1729 and 1323, I will wait for the respective claimants (@Shreyas Srinivas and @Bernhard Reinke ) to weigh in; they may wish to initiate their own summary threads, or report back here on their progress, or do something else.

[Daniel Weber]

Pace Nielsen said:

Specifically, I'm thinking about n = 10, 13, 16, 19, 22.

It doesn't seem to imply any of them

[Shreyas Srinivas]

Sounds good to me. I will probably report success/failure by end of the week. I am still getting comfortable with some of these ATPs which are new to me

[Bernhard Reinke]

I will a do a write-up for my progress so far on 1323, I am hopeful that a "Matrix Greedy" argument might work

[Terence Tao]

Sounds good. Looks like we will need to have a lot of focus on 1485 and 1516 anyways, so I think there is no urgent rush to start threads on 1729 and 1323. Might be a good way to contrast "fast collaborative" with "slow individual" ways of doing mathematics - I believe neither is strictly better than the other, but are instead complementary...

[Terence Tao]

A minor observation: the recent upload of the three finite examples using the FME instructions has caused the number of explicit anti-implications in the codebase to tick up by about 4000. I guess at some point one can perform another transitive reduction to reduce this (and, now that duality is basically implemented within Lean, we could do a further reduction by duality to cut the number of explicit implications and anti-implications by another factor of two). But this is a low priority right now, I don't think this is the bottleneck in CI currently for instance.

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

Terence Tao said:

A minor observation: the recent upload of the three finite examples using the FME instructions has caused the number of explicit anti-implications in the codebase to tick up by about 4000. [...]

This didn't happen because of those 3 examples; the increase would have been trivial. Instead, equational#721 regenerated plan.txt after folding a whole bunch of Vampire disproofs into All4x4Tables. The result was a radically different plan compared to last time.

This was a smart move: re-running the planner is generally a Good Idea™ when lots of new counterexamples are added to All4x4Tables. But something resulted in a plan that let to more explicits this time. There are several possibilities:

1. The input to the planner was much bigger than the one we used last time, and the heuristics that generate the plan didn't cope well so with that.
2. The fitness function in the planner itself does not aim to minimize the number of non-implications that are proven implicitly, but rather the number of checks that the kernel has to do if everything is proven explicitly (checking that some 4-variable equation P holds on a 16x16 magma is rather slow, so the planner prefers to avoid refutations of the form P -> ... in such magmas if possible). Then, the transitive closure computation separately determines what will be shown explicitly and implicitly. This had some good synergy so far, but that might have broken down with this new plan.

I think the right thing to do will be:

• Short-term: start with the previous, better plan, and let the planner update it incrementally. That'll involve somebody (probably me) writing some additional code so that the planner can read and load the preexisting plan (the rest of the required functionality is already there). But I won't be able to work on this until I'm back in full capacity (not for another 1-2 weeks).
• Longer-term: unify the planner and the transitive closure / duality computation, and compute one final plan which is really good. This should set things up for eventual "add more equations" phases of the project as well. I guess I could do this in Lean, and then we'll no longer need the Haskell finite_magma_tools.

[Terence Tao]

OK. It's not urgent, so I've opened equational#725 as a long-term issue to implement your final proposal.

[Jose Brox]

Terence Tao ha dicho:

There is a very similar triality between 1323 (Ly​Ry​Ly2​=I), 1526 (Ly2​Ly​Ry​=I), and 2744 (Ry​Ly2​Ly​=I). Graphiti. For instance, all three laws are equivalent on finite magmas. I am open to suggestions for names for this trio.

I propose to name some of the outstanding equations by looking at the year given by their name. For example, since 1526 marks the death of Scipione del Ferro, I propose to call that trio the del Ferro, Cardano, Tartaglia trio.

In a similar spirit, for 1516 I propose Utopia (since the book by Thomas More was published that year) and for 854 Yongjusa, the Dragon Jewel Temple in South Korea (founded in 854).

[Eric Taucher]

Terence Tao said:

I am open to suggestions for names for this trio.

Minor planet (asteroid)
1323 - Tugela
1526 - Mikkeli - Note: Could not find this in the English version of Wikipedia.
2744 - Birgitta

[Jose Brox]

Any opinions on the names @Eric Taucher and I suggested above? @Terence Tao

[Terence Tao]

To be honest, now that we are down to three unsolved equations, "Ramanujan" 1729, 1323, and 1516, I have found it less necessary to come up with suitable names to distinguish them, particularly since they seem to share a lot of commonality anyway.

[Jose Brox]

Terence Tao ha dicho:

To be honest, now that we are down to three unsolved equations, "Ramanujan" 1729, 1323, and 1516, I have found it less necessary to come up with suitable names to distinguish them, particularly since they seem to share a lot of commonality anyway.

I was doubting if we would choose practicality (the right now) or consistency (the future), since other identities already have names that may appear elsewhere, which perhaps may end up seeming a bit random.

[Bernhard Reinke]

Pace Nielsen said:

1722 also fell. I'll check 1518 later when I have some time.

1722.pdf
1722.tex

The initial seeds don't seem to work directly in the free group. I haven't looked at why yet, hopefully one just needs to enlarge it slightly.

[Bernhard Reinke]

One has less freedom for the initial seed that I hoped, (1,x₁),(x₁⁻¹,x₂) ∈ E forces (x₂,x₁⁻¹),(x₁⁻¹*x₂⁻¹,x₁*x₂⁻¹),(x₁,1),(x₁^(-2),x₁^(-2)) (only using the translation invariant version of 1722), in particular, there is no translation invariant counter example showing 1722 !=> 2644. I will have a look at the other implications to see whether they are still ok. But I guess we need the non-translation invariant greedy version for 1722 at some point anyway.

[Bernhard Reinke]

3050 also doesn't work

[Pace Nielsen]

I'll look at this when I get a chance later today. It looks like I made a mistake in the initial seed.

[Pace Nielsen]

1722->1832 also doesn't work. It appears that 1722 is still wide open. The translation invariant approach won't solve these implications.

[Shreyas Srinivas]

Wait so we have more open implications now?

[Pace Nielsen]

Yes, that is correct.

[Shreyas Srinivas]

Is there a TL DR of the translation invariant apprpach and why it fails?

[Shreyas Srinivas]

I assume some of this material is already in the blueprint

[Terence Tao]

We have a non-translation-invariant approach to 1722. The following seed seems to refute all implications:

$0 \diamond 0 = 1, 0 \diamond 1 = 5$
$1 \diamond 0 = 2, 1 \diamond 1 = 7, 1 \diamond 2 = 0, 1 \diamond 3 = 1, 1 \diamond 4 = 2$
$2 \diamond 0 = 3$
$3 \diamond 0 = 4$
$5 \diamond 1 = 6$
$7 \diamond 0 = 10, 7 \diamond 1 = 8, 7 \diamond 6 = 0, 7 \diamond 8 = 1, 7 \diamond 9 = 7$
$8 \diamond 1 = 9$

[Terence Tao]

Shreyas Srinivas said:

Is there a TL DR of the translation invariant apprpach and why it fails?

The Asterix, Obelix, and Dupont translation invariant greedy constructions in Chapter 7 of the blueprint are pretty representative. The failure tends to just be some algebraic computation in which one takes the functional equation for $f$ in the translation invariant model and substitutes in a few values and see what happens, one could possibly even automate this procedure with an ATP to find translation immunities. Sometimes one can also get translation immunity from the fact that squaring (or other single-variable word maps) are necessarily bijections in these models.

[Matthew Bolan]

Doesn't this violate law 1 at (0,0)? ((0 ◇ 0) ◇ 0) = (1 ◇ 0) = 5 is defined, but (0 ◇ 0) ◇ 5 = 1 ◇ 5 is not defined.

[Terence Tao]

Oh right I screwed things up a fair bit (mixed up left and right multiplication, ugh.). One sec. EDIT: hopefully fixed now.

[Matthew Bolan]

My code says you have a violation at x,y = 1,3 if I've entered it in correctly. $(1 \diamond 3) \diamond 3 = 1$ is defined, so we need to add in at least a $3 \diamond 3$

[Matthew Bolan]

If I add that in naively I get a similar problem at 7, 9

[Terence Tao]

You're right. It seems that I'm going to need to reuse some elements in order to get things to close. Have to step away for a bit, but will try again later.

[Matthew Bolan]

I've run out of time so I can't finish the code (In particular I am not using any ATP nor am I simulating the greedy algorithm yet), but I think its at least found a repair for 1832.

Failure of Equation1832[x = (x ◇ (x ◇ x)) ◇ (x ◇ x)] at 1
0 1 1 _
3 0 _ _
_ _ _ _
2 _ _ _

[Matthew Bolan]

(It also found tables for 3143 and 2737, but these are implied by the others)

[Terence Tao]

The most difficult refutation is 2644, because the existence of $S^2 x$ ends up causing quite a bit of propagation. If we set $Qx := (Sx \diamond x) \diamond x$ then one can use the 1722 law to work out the identities $Sx \diamond Qx= Sx$, $SQx \diamond Sx = Sx$, and $SQx = S^3 x$. These laws then iterate, for instance we have $SQS^a x = S^{a+3} x$ and so forth. If one adds the simplifying rule $Q^2 = 1$ then one can create an infinite seed with elements $S^a x, QS^a x$ for $a \geq 0$, together with some additional elements $y_a, z_a$ for $a \geq 0$, obeying the following table:
$S^a x \diamond S^a x = S^{a+1} x$
$QS^a x \diamond QS^a x = S^{a+3} x$
$S^{a+1} x \diamond S^a x = y_a; \quad y_a \diamond S^a x = QS^a x$
$S^{a+3} x \diamond QS^a x = z_a; \quad z_a \diamond QS^a x = S^a x$
$S^{a+1} x \diamond QS^a x = S^{a+1} x$
$S^{a+3} x \diamond S^a x = S^{a+3} x$
$S^{a+3} x \diamond S^{a+1} x = S^{a+1} x$
$S^{a+1} x \diamond S^{a+3} x = S^{a+3} x.$
I think this verifies all the seed axioms, but is of course infinite. One can reduce to a finite model by setting $S^{a+4} x = S^{a} x$, $QS^{a+4} x = QS^a x$, $y_{a+4} = y_a$, $z_{a+4} = z_a$ for all $a \geq 1$, which leaves one with I think 20 elements as now $a$ is restricted to $0,1,2,3,4$. To get failure of 3050, $Qx \diamond x = x$, one can then add an additional rule $Qx \diamond x = u$ for some new element $u$; to get failure of 1832, $x = (x \diamond Sx) \diamond Sx$ one can add additional rules $x \diamond Sx = v$, $u \diamond Sx = w$ for some new elements $v,w$; and to get failure of 2644, $S^2 x \diamond x = x$ one can add an additional rule $S^2 x \diamond x = r$ for some new element $r$. I think this creates a single seed (with 24 elements!) that refutes all the rules.

[Matthew Bolan]

If I understand correctly, $(S^0x \diamond S^0x ) \diamond S^0x = S^1 x \diamond S^0x = y_0$, so 1722 requires $(S^0x \diamond S^0x ) \diamond y_0 = S^1x \diamond y_0$ to be defined, which it doesn't seem to be to me.

[Matthew Bolan]

Went ahead and finished my finder.

Failure of Equation2644[x = ((x ◇ x) ◇ (x ◇ x)) ◇ x] at 0
========
1 _ _ _
2 2 0 1
3 1 2 3
_ _ _ 2
========
Failure of Equation3050[x = (((x ◇ x) ◇ x) ◇ x) ◇ x] at 0
==========
1 _ _ _ _
2 _ 0 1 2
3 1 2 3 _
4 _ _ 2 _
_ _ _ _ _
==========

[Terence Tao]

I was going to say that my seed could probably be fixed by adding $S^{a+1} x \diamond y_a = S^a x$ and $S^{a+3} x \diamond z_a = QS^a x$, but now that you found quite simple seeds, this is now moot :)

[Matthew Bolan]

Yes, my program says that does repair it.

[Matthew Bolan]

Looks like the table

1 2 _ _ _
2 3 0 1 2
3 4 _ _ _
4 1 _ 3 0
_ _ _ _ _

gets all of them in one shot (all counterexamples have all variables equal to 0).

[Terence Tao]

Uploaded the proof of 1722 to the blueprint at equational#862.