About 1729 vs 817

Stream: Equational

[Shreyas Srinivas]

So I don't have much time and I only got to work on this equation with z3 since the middle of this week. This list isn't complete even with what I have now. So far I have some rather trivial insights:

1. Firstly I chose z3 because it had an easily accessible python API. I believe it is not too hard to adapt this to cvc5 since that one has a nearly identical python API.
2. I have conducted most of my runs on Ints as the canonical infinite domain.
3. A few trivial things that I think are already known or easily visible by a quick glance at the equations: the binary operation of the Magma refuting the implication has to be : non-associative, non-commutative, non-idempotent. Further it cannot have a left identity.
4. I have a conjecture based on experiments that restricting the range of values of $x$ or $y$ from above and below, within which they can deviate from the projection operations does not yield a counterexample. EDIT : z3 confirms this.

I will add more in the next few days to the above. In addition, and to a smaller extent, I have basically been trying to apply the methods of 1323 to this and none of the methods have yielded a counterexample so far. That being said, my goal there was to replicate the methods, and it was easiest to do so on finite examples and we don't expect finite counterexamples for this one.

[Shreyas Srinivas]

The reason I checked the last point is the way z3 was presenting its models of functions: A tabulation of values for small integers and a projection function for all other values.

[Shreyas Srinivas]

Point 4 above and some basic runs on z3 suggest to me that Integers (although SMT solvers have a great theory for them usually) are poor candidates for finding a counterexample. For instance, a few days ago z3 and cvc5 had a lot of trouble trying to find an operation satisfying 1729 (which is trivially satisfied by subtraction) without extra hints.

[Shreyas Srinivas]

Lastly, apologies for not getting to this earlier. I have been under extreme time constraints. Also, if any of this gets double posted, I am sorry about that too. Zulip's android app gives me a lot of trouble in this department

[Terence Tao]

Thanks for the update! I am suspecting that if one is to try to import the latest 1323-solving technology to 1729, one will need a good "base model" for 1729 on the squares, which would not directly refute 817, but could then be extended to non-squares. Looking forward to the full update!

Perhaps in the meantime, the following prepatory questions could be answered through ATPs, in analogy with how they laid the groundwork for the 1323 solution:

1. Is it safe to assume that the 1729 model is unital? Does this lead to simpler formulations of the 1729 law?
2. Is it safe to assume that the set $SM$ of squares is closed under multiplication?
3. Is it ruled out that the squares could be constant? What if the squares take only two values $+1,-1$?

[Shreyas Srinivas]

A small extension to the update : In my pen and paper work I wanted to find a natural way to create non-associative operations from simple ones. I came up with a "stateful operations" heuristic to do this. The idea comes to me from basic ML theory, where a larger hypothesis space is defined by parametrising over a smaller hypothesis space. (EDIT: In hindsight, it seems this can also be motivated by concurrency race conditions). The point is to have a bit more parametric control over the binary operation with the hope that SMT solvers have less trouble performing a parameter search than an uninterpreted function search for the full binary operation. All this is still a bit hazy and I want to run this on z3 and cvc5.

To give a trivial but illustrative example of this statefulness: Suppose the underlying domain is $Int \times Bit$. Suppose $(x, s_1) \diamond (y,s_2)$ is defined as $(x \circ y, s_1 \oplus s_2\oplus 1)$ where $\circ = +$ when $s_1 \oplus s_2 = 0$ and $\circ = -$ otherwise. Then $(x, 0) \diamond ((y, 0) \diamond (z,0)) = (x - y - z, 0)$ whereas $((x,0) \diamond (y,0)) \diamond (z,0)$ will be $(x + y -z, 0)$. The intuition here is that the state $Bit$ tracks the parity of number of operation uses and the use of non-associative operations in some cases ensures that the order of application of the individual instances $\diamond$ makes a difference.

[Shreyas Srinivas]

Terence Tao said:

Thanks for the update! I am suspecting that if one is to try to import the latest 1323-solving technology to 1729, one will need a good "base model" for 1729 on the squares, which would not directly refute 817, but could then be extended to non-squares. Looking forward to the full update!

Perhaps in the meantime, the following prepatory questions could be answered through ATPs, in analogy with how they laid the groundwork for the 1323 solution:

1. Is it safe to assume that the 1729 model is unital? Does this lead to simpler formulations of the 1729 law?
2. Is it safe to assume that the set $SM$ of squares is closed under multiplication?
3. Is it ruled out that the squares could be constant? What if the squares take only two values $+1,-1$?

This sounds like a good starting point. I'll try these out

[Terence Tao]

This seems to align with some of the strategies we've tried successfully for other equations in which we assume there is a homomorphism from the desired magma to some small base magma (such as $Bit$) which often seems to clarify the algebra and enforce some good structural properties.

[Shreyas Srinivas]

Right, so I am approaching this from the point of view "What natural operations in computer science would not have the usual algebraic properties". It is trivial to find non-commutative operations (any monad would do). But non-associativity is much harder, since almost every nice data structure I can think of in CS has some sequential composition notion which corresponds to associativity. Things change when one adds statefulness

[Shreyas Srinivas]

and then the challenge is to start with basic non-associative operations and build more complex ones, and parametric ones.

[Shreyas Srinivas]

I think I ruled out the squares being +/-1 already, but I'll add an experiment to my notebook again to confirm this.

[Shreyas Srinivas]

Terence Tao said:

1. Is it safe to assume that the 1729 model is unital? Does this lead to simpler formulations of the 1729 law?

Since I haven't been in a math dept for a while, I am guessing by unital you mean it has an identity element with left and right identity laws. The left identity law is ruled out. Having a right identity hasn't yielded much so far.

[Shreyas Srinivas]

basically 1729 is not consistent with a left identity rule

[Shreyas Srinivas]

Another observation, for the fallback conditions, when beyond a certain range of values of $x$, I implement subtraction as a fall back rule, even for large limits I get unsatisfiability. But when I turn the limit into a variable z3 can't find it. This wasn't the case when the fallback rules were projections

[Shreyas Srinivas]

The right identity law is also inconsistent with 1729

[Terence Tao]

OK, so imposing units is a bust. Good to know!

[Shreyas Srinivas]

I take that last one back. right identity is not confirmed yet. I had a minor error

[Terence Tao]

Another possible simplifying assumption is $S^2 = S$, i.e., squares are idempotent (equation 151), or $S^2 = 0$ for some constant $0$ (which will necessarily equal the right identity, if it exists).

[Shreyas Srinivas]

I already tried idempotence. I am currently on my machine and setting up everything in my notebook but not running any solver longer than 2 minutes.

[Shreyas Srinivas]

So far all the indeterminate runs have been run under 2 minutes.

[Shreyas Srinivas]

$S^2 = e$ is ruled out for any constant $e$

[Shreyas Srinivas]

Based on my experience so far, positive constraints narrow down the search much more quickly than negative constraints.

[Shreyas Srinivas]

at least positive equational constraints. This intuitively makes sense.

[Terence Tao]

Perhaps the most important remaining constraint to test is whether $SM$ can be closed: the product of two squares is always a square. This seems rather key if one is to try a "build the multiplication table on the squares first" approach.

[Shreyas Srinivas]

Running it. I'll report back in a few hours.

[Ted Hwa]

Right identity is ruled out (assuming you are looking for a counterexample) since in equation 1729, $x = (yy)((yx)y)$, if 1 is a right identity, then substituting x=1 gives $1 = (yy)(yy)$. Then equation 817 $x = x((xx)(xx))$ becomes $x = x1$ which is true.

[Shreyas Srinivas]

That's my idea too but I want to coax z3 to say so

[Shreyas Srinivas]

In my earlier attempt I had forgotten to remove a different constraint which gave unsat

[Shreyas Srinivas]

Further attempts on left identity have shown too much variance in running times.

[Shreyas Srinivas]

And z3 didn't terminate the right identity for a long while

[Ted Hwa]

Vampire finds the proof for right identity instantly.

[Shreyas Srinivas]

Interesting. What's the ground theory you are using?

[Shreyas Srinivas]

Does vampire have some inbuilt support for equational reasoning that smt solvers don't?

[Ted Hwa]

I'm not familiar with internals of Vampire but I believe it does have support for equational reasoning, based on the proof it outputs.

[Ted Hwa]

The proof from Vampire is basically the same as the one I wrote above.

[Shreyas Srinivas]

Does vampire have an easy API in other languages

[Shreyas Srinivas]

So far I haven't seen anything in that direction. I will also try cvc5

[Ted Hwa]

It doesn't seem to have an API for other languages, only its own CLI interface

[Shreyas Srinivas]

Oh that's sad. I was hoping I could just plug it into a jupyter notebook. So far with z3 and a bit of cvc5, it has been very useful

[Terence Tao]

I suspect the 3-step procedure used to resolve 1516->255 has a good chance of working for 1729->817. The steps are:

1. First build a 1516 model $SM$ for the squares, with some additional properties TBD (analogous to the "double surjectivity" in the 1516 case) required to advance to step 2. In particular, the $SM \times SM$ block of the multiplication table is now filled in: we understand "squares x squares".
2. Work out the $SM \times (M \backslash SM)$ and $(M \backslash SM) \times M$ blocks of the table ("squares x non-squares" and "non-squares x squares"). Here I think we mostly rely on the form $L_{Sa} R_a L_a = 1$ of the 1729 law for $a \in SM$. For squares, all the left and right multiplication operators are invertible, so for instance $R_a = L_{Sa}^{-1} L_a^{-1}$, which tells us that the "non-squares x squares" block of the table is determined by the "squares x non-squares" block. Some additional properties (analogous to the "infinite surjectivity" in the 1516 case) need to be imposed to advance to step 3.
3. Fill in the last block $(M \backslash SM) \times (M \backslash SM)$ of the multiplication table. This should be relatively straightforward because 1729 now reduces to a law of the form $(y \diamond x) \diamond y = \hbox{known}$ which looks easy to fill in greedily, assuming that we have had the foresight to implement some suitable "infinite surjectivity" type hypothesis in step 2.

[Shreyas Srinivas]

Ted Hwa said:

Right identity is ruled out (assuming you are looking for a counterexample) since in equation 1729, $x = (yy)((yx)y)$, if 1 is a right identity, then substituting x=1 gives $1 = (yy)(yy)$. Then equation 817 $x = x((xx)(xx))$ becomes $x = x1$ which is true.

Btw, to put it out there, this argument is important in my argument for left identity being inconsistent with 1729, since if there was a left identity, $1_L$, using $y= 1_L$ in 1729, it reduces to $x = x \diamond 1_L$ for every $x$. Now this makes $1_L$ a right identity.

[Shreyas Srinivas]

Which in turn is inconsistent with negating 817

[Shreyas Srinivas]

One thing I must note is that z3 has been behind my mental math in almost all observations. The exception is the refutation of some fallback based operations.

[Shreyas Srinivas]

Terence Tao said:

I suspect the 3-step procedure used to resolve 1516->255 has a good chance of working for 1729->817. The steps are:

1. First build a 1516 model $SM$ for the squares, with some additional properties TBD (analogous to the "double surjectivity" in the 1516 case) required to advance to step 2. In particular, the $SM \times SM$ block of the multiplication table is now filled in: we understand "squares x squares".
2. Work out the $SM \times (M \backslash SM)$ and $(M \backslash SM) \times M$ blocks of the table ("squares x non-squares" and "non-squares x squares"). Here I think we mostly rely on the form $L_{Sa} R_a L_a = 1$ of the 1729 law for $a \in SM$. For squares, all the left and right multiplication operators are invertible, so for instance $R_a = L_{Sa}^{-1} L_a^{-1}$, which tells us that the "non-squares x squares" block of the table is determined by the "squares x non-squares" block. Some additional properties (analogous to the "infinite surjectivity" in the 1516 case) need to be imposed to advance to step 3.
3. Fill in the last block $(M \backslash SM) \times (M \backslash SM)$ of the multiplication table. This should be relatively straightforward because 1729 now reduces to a law of the form $(y \diamond x) \diamond y = \hbox{known}$ which looks easy to fill in greedily, assuming that we have had the foresight to implement some suitable "infinite surjectivity" type hypothesis in step 2.

Sounds like a plan, although I should probably do this tomorrow. It is rather late now in my part of the world.

[Shreyas Srinivas]

It is possible I need to tweak/improve my way of using these SMT solvers, as the same heuristics don't seem to translate one-one to other ATPs

[Shreyas Srinivas]

I have been doing some not yet successful pen and paper work building off my "stateful operation" heuristic. At first glance this heuristic appears to allow us to have heterogeneous operations whose effect depends on the position of the operator's occurrence in the abstract syntax tree (AST) of an expression. For instance if one looks at the height of the operators in equations 817 and 1729. Let's use subtraction as our basic operation. Looking at the ASTs of 817 and 1729, it is clear that if we apply flipped subtraction ($x \diamond y = y -x$) at height 3 nodes, we can break 817 and we can fix this breakage in 1729 by using flipped subtraction in height 1 nodes. For height 0 nodes we use normal subtraction.

However this is not enough. We homogenise these heterogeneous operations by encoding some extra data in the operands (for example by adding a height modulo 3 parameter to the domain) that carries some info about the . The operation itself needs to be defined uniformly on inputs regardless of the input height parameter. In particular 1729 must be satisfied independent of the height parameter component of the input arguments to the parameters $x$ and $y$. nFor example a user might give an equation in which 1729's rhs is a subterm whose root occurs at height 5. It might receive as input values with varying heights. The goal is to get a better operation that is uniform w.r.t. input "heights"

[Shreyas Srinivas]

Maybe height of the operand node is the wrong parameter to focus on, although it seems easiest.

[Jose Brox]

Terence Tao ha dicho:

1. Is it ruled out that the squares could be constant? What if the squares take only two values +1,−1?

Only two squares is quickly ruled out by Vampire-SAT (as expected, Prover9 is still running on it after 8 minutes...).

[Terence Tao]

@Shreyas Srinivas does it look like your stateful operation constructions could at least produce interesting infinite models of 1729 even if they cannot fulfill 817? They may be useful recipes for step 1 of the three-step procedure I mentioned previously.

If we wanted to pursue the 3-step strategy more, I think the first thing to do is focus on step 3: assuming that the multiplication table is already filled in $SM \times M \cup M \times SM$, what axioms need to be satisfied on that portion of the table in order to be able to easily fill in the non-square portion $(M \backslash SM) \times (M \backslash SM)$ by a greedy algorithm? Note that 817 doesn't directly care about this portion, as it can be tested purely using the $M \times SM$ component, so if we can get a clean criterion for solvability of the completion problem of the multiplication table from $SM \times M \cup M \times SM$ to $M \times M$, then this should resolve Step 3 and leave us just with working out the other two steps.

[Shreyas Srinivas]

With my model refuting 817 is easy. It is satisfying 1729 that is more difficult

[Shreyas Srinivas]

Because whatever extra parameters I tack on to integers, 1729 must be satisfied for all possible instantiations

[Shreyas Srinivas]

Basically the only structurally asymmetric occurrence of the operator in 817 is the first instance from the left (or the root of the AST). The modification of this occurence must be compensated for in 1729. In my example above, when using subtraction as a building block, this means flipping the height 2 occurrences

[Shreyas Srinivas]

But satisfying 1729 by itself without worrying about 817 is easy

[Shreyas Srinivas]

Subtraction satisfies it

[Shreyas Srinivas]

It's just not super useful

[Shreyas Srinivas]

Jose Brox said:

Terence Tao ha dicho:

1. Is it ruled out that the squares could be constant? What if the squares take only two values +1,−1?

Only two squares is quickly ruled out by Vampire-SAT (as expected, Prover9 is still running on it after 8 minutes...).

I am really curious as to why vampire seems to be so much more successful than basically any other prover (including in several cases, just pen and paper work).

[Terence Tao]

Are you able to construct a model of 1729 in which the iterated squaring map $S^3$ is non-constant, where $Sx = x \diamond x$ (so $S^3 x = ((x \diamond x) \diamond (x \diamond x)) \diamond ((x \diamond x) \diamond (x \diamond x))$)? I have an idea on how to make the 3-step program work, but it requires a seed model in which $S^3$ is non-constant (more precisely I need the set $\{ S^2 x, S^3 x\}$ to vary in a non-trivial way in $x$, but presumably making $S^3$ non-constant will do this).

[Shreyas Srinivas]

Not yet, but I think there might be a way to do that on pen and paper. Intuitively, I just need to keep track of the number of continuous applications of an element to itself

[Shreyas Srinivas]

And reset the counter on non-contiguous occurrences, and also an extra state variable to keep track of the last value assigned to a cube

[Shreyas Srinivas]

Also keep the starting values of the counters in memory for reference. At this point I am just defining a Moore machine

[Shreyas Srinivas]

Sorry a mealy machine and then convert it to a moore machine.

[Shreyas Srinivas]

And then encode its table in an operator.

[Shreyas Srinivas]

I'll get on with this and report back in a few hours

[Terence Tao]

Actually I think I may just need a model with $S^2$ non-constant (not $S^3$).

The model I have in mind is that of an infinite submagma $SM$ of squares (in which $S^2$ is non-constant, so $S^3$ will be non-constant in the entire magma), and then a larger set $M \backslash SM = SM \times ({\mathbf F}_2^{SM})_0$ of non-squares $(a,x)$, where $a \in SM$ and $x$ is in the free abelian group $({\mathbf F}_2^{SM})_0$ of exponent 2 generated by a generator $e_b$ of order 2 for each $b \in SM$. The squaring map on non-squares is to be given by $S(a,x) = a$, and the left-multiplication by squares $b \in SM$ given by
$L_b (a,x) = (a, x + e_b).$
These operators commute and are involutions, so the Ramanujan law $L_{Sb} R_b L_b = I$ then tells us what the right-multiplication by squares given by
$R_b (a,x) = (a, x + e_b + e_{Sb}).$
If the squaring map is non-trivial enough, one should have $R_b(a,x)$ take different values as $b$ varies. To get a 817 violation we need something like $S^3$ being non-trivial globally, so $S^2$ should be non-trivial on the submagma $SM$.

To fill out the remainder of the multiplication table for non-squares, there is a constraint $R_b (a,x) \diamond (a,x) = L_a^{-1} b$, and 1729 for non-squares basically reduces to the law
$(a,x) \diamond (b,y) = (c,z) \implies (c,z) \diamond (a,x) = (b, y + e_a).$
This law iterates to produce 6-cycles similar to the 1323 construction, so I think there is a good chance of filling out the table by a greedy construction.

[Shreyas Srinivas]

I will need a bit more time. But I have had many false starts on the domain $Int \times \{0,1,2\}$ where the latter set has the usual order but increment and decrement, and consequently addition and subtraction wrap around (basically all operations on the second element are modulo 3). Intuitively, when the absolute value of height difference (denoted by 0,1,2). The base operation is subtraction of reals. To satisfy 1729, one must encoded that if the height difference on the left and right are 0 then apply normal subtraction whereas when they are not, apply flipped subtraction.

An alternative is that at 0 height difference apply flipped subtraction, at height diff 1, apply addition, and at height difference 2 apply normal subtraction. This can get a non constant square operation. The challenge is to figure out the correct formulation for the new height of the result of the operation. This has been my last few hours of work. At times it has taken me tantalising close to an answer only for me to find out that for each height assignment I have constructed so far, EQ 1729 breaks at some place or the other

[Shreyas Srinivas]

Breaking 817 is easy. So far I have been exploiting the only asymmetry in 817 which is the height 2 occurrence of $\diamond$, and I am using it as a guideline for constructing the conditional statement for switching operations.

[Shreyas Srinivas]

I am a bit tied up for the next 3 days. I'll post an update on Sunday. Hopefully I have a way to safely handle bad state inputs by then

[Shreyas Srinivas]

In the meantime, when I have a half an hour here or there to spare, I will try to post some of the simple examples as lean code here, so that others can modify and play with the idea.

[Terence Tao]

If constructing a base model is too hard, it may be possible to pull off a "swindle" and perform an infinite number of extensions to get a non-trivial model, without ever having to verify the base model properties at all, by pushing the base model further and further back in "time" and passing to the limit. I haven't really thought this idea through, but I guess we'll see first how the efforts to build non-trivial 1729 models are going.

[Matthew Bolan]

Did the recent correction to the argument for 1323 impact the idea to build a 1729 -> 817 counterexample from a model with $S^2$ non-constant?

[Terence Tao]

I think 817 has a different flavor to 2744, it only needs the "non-squares x squares" portion of the multiplication table rather than the "non-squares x non-squares" to refute. But I haven't worked out any details yet.

[Terence Tao]

Here is a negative result: if one has $S( x \diamond S^2 x ) = S x$, then 817 holds. So this actually rules out the type of models used for 1323, as they obey this rule (at least for non-squares, in fact the model obeys the stronger law $S(x \diamond Sy) = S(Sy \diamond x) = Sx$ for non-square $x$); we need to find a more complex model that avoids this rule.

Proof: 1729 states that $L_{Sy} R_{y} L_y x = x$. Setting $y=x$ we obtain $L_{Sx}^2 x = x$. Next, replacing $x,y$ by $S^2x, x$ we have $L_{Sx} (R_{S^2 x} x \diamond x) = S^2 x$, so $R_{S^2 x} x \diamond x = Sx$ by invertibility of $L_{Sx}$. Replacing $x,y$ by $x, R_{S^2 x} x$ and using the hypothesis we have $L_{Sx} R_{R_{S^2 x} x} Sx = x$, hence $L_{Sx}^2 R_{S^2 x} x = x = L_{Sx}^2 x$. By invertibility of $L_{Sx}$ we conclude $R_{S^2 x} x = x$, but this is 817. $\Box$

Conversely, 817, which is $x \diamond S^2 x = x$, clearly implies $S( x \diamond S^2 x ) = S x$. So it is really the law $S( x \diamond S^2 x ) = S x$ that needs to be refuted, rather than $x \diamond S^2 x = x$.

[Terence Tao]

It may be useful to repeat the ATP-assisted exercise we have done in similar equations of trying to find additional axioms we can place on top of 1729 that can simplify the algebra without accidentally proving 817. So for instance $S(x \diamond S^2x) = Sx$ would be an example of an axiom that we cannot impose; the laws $S L_{Sy} x = Sx$ and $S R_{Sy} x = Sx$ similarly cannot be imposed (the former implies the latter since $R_{Sy} = L_{S^2y}^{-1} L_{Sy}^{-1}$).

[Terence Tao]

Another observation: the identity $R_{S^2 x} x \diamond x = Sx$ just proven shows that the law 817 holds whenever $R_x$ is injective, in particular 817 holds for squares.

[Shreyas Srinivas]

I will have time to do this tomorrow. I'll try to run multiple ATPs

[Terence Tao]

Thanks! Some sample questions that ATPs may be able to answer (with partial confidence):

• Can we assume that squares are closed under multiplication, i.e., that for all $x,y$ there exists $z$ such that $Sx \diamond Sy = Sz$?
• Can we assume there a right unit $x \diamond 0 = x$? What about a left unit $0 \diamond x = x$ (which I think is stronger)?
• Can we assume $S^2$ is a constant? (Probably not.) What about $S^3$? Or maybe $S^2 = S$ or $S^3 = S^2$ could be viable axioms.
• Could left-multiplication by squares be abelian, thus $Sx \diamond (Sy \diamond z) = Sy \diamond (Sx \diamond z)$? This would also imply that right multiplication on squares is abelian. Separately, could we assume that left-multiplication by squares is an involution, $Sx \diamond (Sx \diamond y) = y$?

[Shreyas Srinivas]

Infinitesimal update: many z3 runs ongoing. I think I already ruled out $S^2$ being constant because in 817, $S^2(x)$ would become an identity element, and our elusive counterexample can have neither left nor right identity

[Shreyas Srinivas]

Further, higher up in the thread we already have proofs that we can't have a right or left identity (one follows from the other)

[Shreyas Srinivas]

I think I am going to add to my list the following check: whether I can satisfy the one variable variant of 1729

[Shreyas Srinivas]

It won't be a valid counter example, but it might prune the search a bit

[Shreyas Srinivas]

My editor crashed with the square closure run (I am running z3 inside vscode)

[Shreyas Srinivas]

If $S^3$ is a constant, then even square elements cannot have a right identity (substituting $Sx$ in 817)

[Shreyas Srinivas]

left multiplication being involutive is consistent with 1729, but does not imply it fully. It doesn't seem inconsistent with 817

[Terence Tao]

Just reporting what would be needed to extend a base 1729 magma $SM$ (representing "squares") to a larger magma $M = SM \uplus N$ (with $N$ representing "nonsquares"), thus we are restricting attention to models where the set of squares $SM$ is closed under multiplication, and is already given to us somehow.

I will consistently use $a,b,c$ for elements of $SM$ and $x,y,z$ for elements of $N$ (or $M$). This requires introducing a squaring map $S: N \to SM$ and to complete the original mutiplication table $\diamond: SM \times SM \to SM$ to $M$. From the bijective nature of $L_a, R_a$ for $a \in SM$ we know that these maps have to permute the non-squares, thus we have to define bijections $L_a, R_a: N \to N$ as well as the multiplication operation $\diamond: N \times N \to M$ for non-squares.

1729 asserts that $L_{Sy} R_y L_y = 1$. For squares $a \in SM$, we can rearrange this as

$R_a = L_{Sa}^{-1} L_a^{-1}\quad (1).$

Thus the right-multiplication operators $R_a: N \to N$, $a \in SM$ are completely determined by the left-multiplication operators $L_a: N \to N$, $a \in SM$.

Applying 1729 with $y \in N$ and $a \in SM$, we obtain $L_{Sy} R_y L_y a = a$, which we can rearrange as
$R_a y \diamond y = L_{Sy}^{-1} a \quad (2).$
This fills out part of the multiplication table on $N \times N$. One has to ensure that this rule does not collide with itself, or with the consistency condition
$y \diamond y= Sy \quad (3)$
so we need the $R_a y$ to be distinct from each other and from $y$ as $a \in SM$ varies (an exception can be made if $a = S^2 y$, but we do not want to make this exception for all $y$ as this would precisely give 817).

1729 can also be written as
$y \diamond x = z \implies z \diamond y = L_{Sy}^{-1} x.$
Applying this with (3) and $y \in N$ we obtain the constraint
$L_{Sy}^2 y = y \quad (4)$
so $y$ is either a fixed point or a 2-periodic point of the permutation $L_{Sy}: N \to N$. Applying this instead with (2),we obtain
$L_{L_{Sy}^{-1} a} R_a y = L_{SR_a y}^{-1} y$
for $y \in N$ and $a \in SM$. We can change variables a bit and write this constraint as
$L_{SR_{Sy \diamond a} y} L_a R_{Sy \diamond a} y = y \quad (5).$
It was tempting to simplify this law by asking that right-multiplication did not affect squares, so that $SR_{Sy \diamond a} y = Sy$. But then (5) and (4), together with the invertibility of $L_{Sy}$, would simplify to
$L_a R_{Sy \diamond a} y = L_{Sy} y$
and setting $a = Sy$ we would obtain
$R_{S^2 y} y = y \quad (817)$
which is 817. So we need right-multiplication to affect squares at least once .

Anyway, I believe (1), (4), (5) are the main constraints. If we can find a base 1729 magma $SM$ and left and right multiplication operators $L_a, R_a: N \to N$ for $a \in SM$ obeying (1), (4), (5) but not (817), and with the $R_a y$ distinct from each other and from $y$ as $a$ varies, then we should be able to greedily fill in the rest of the table (providing $N$ is infinite and nothing too bad happens with the iteration).

[Terence Tao]

For the record, we have the following non-trivial model of 1729, which unfortunately obeys 817, but could potentially be a base model for a larger 1729 magma that violates 817.

Let $G$ be a countably infinite abelian group of exponent 2. The carrier is $G \times G$. The multiplication law is partially given by
$(x,a) \diamond (b,0) = (b,0) \diamond (x,a) = (x+b, a)$
$(x,a) \diamond (x+b,a) = (a+b,0).$
So in particular $S(x,a) = (a,0)$. For the remaining products $(x,a) \diamond (y,b)$ with $a,b,0$ distinct, these should be set to $(z,c)$ for some $c$ distinct from $a,b,0$ subject to the rule
$(x,a) \diamond (y,b) = (z,c) \implies (z,c) \diamond (x,a) = (y+a,b).$
This is a 6-periodic rule and can be filled out by the usual greedy algorithm.

It is not difficult to check that this obeys 1729. Unfortunately it also obeys 817: $S^2 (x,a) = (0,0)$ and $(x,a) \diamond (0,0) = (x,a)$ for all $x$. But perhaps we can use it as a base for a more sophisticated model.

If $G$ is a boolean algebra, we can in fact choose the explicit form
$(x,a) \diamond (y,b) = (x+y+ab, a+b)$
which I think was also observed in the 1323 thread by @Bruno Le Floch .

[Shreyas Srinivas]

If $G$ is a Boolean algebra, this operation is commutative

[Shreyas Srinivas]

So we have a lot to undo if we start there

[Terence Tao]

I am thinking of using this as a model just for the squares. If ATPs do not rule out the possibility of the squares being commutative, closed under multiplication, and unital, then having a boolean model for the squares may be viable.

[Terence Tao]

The squares would also obey $S^2=0$, so the general magma would obey $S^3=0$, but to my knowledge this has not been ruled out. (Also, $0$ is only a unit within the squares; it is not required to be a unit in the larger magma, and probably we would have to abandon that property.)

[Terence Tao]

Hmm, but I see from your previous post that one cannot have $S^3=0$ and $0$ a unit for the squares, so indeed the boolean model cannot serve as a base model. (But it could perhaps be a base for a base...)

[Terence Tao]

Hmm maybe you can clarify actually: if $S^3= 0$ and $0$ is (say) a right unit for the squares, were you able to show that this implies 817 for all elements, or only for the squares? For if it is just the latter, we could still hope to use the boolean model as the base model to produce at least one contradiction to 817 (we don't need to contradict it everywhere, and I think in fact it automatically holds for squares in any case).

[Terence Tao]

The boolean example is also an abelian group of exponent 4, and conversely addition on any abelian group of order 4 is a 1729 magma (funny how I never noticed that before).

[Shreyas Srinivas]

So far I have not refuted identity elements on either side for only squares, only that they must exist

[Shreyas Srinivas]

The square closure is giving my z3 installation quite a bit of trouble

[Shreyas Srinivas]

It could just be that I am using an underpowered machine/software setup

[Shreyas Srinivas]

$S^3=0$ means that all square elements must satisfy 817 trivially.

[Terence Tao]

In fact I believe 817 holds for squares (i.e. $Sx \diamond S^3 x = Sx$) even without any additional axioms beyond 1729, because we have $(x \diamond S^2 x) \diamond x = Sx$, hence $R_{Sx} (Sx \diamond S^3 x) = R_{Sx} Sx$, hence $Sx \diamond S^3 x = Sx$.

[Shreyas Srinivas]

I don't quite see it right away. In the first step you have multiplied both sides of 817 by x.

[Shreyas Srinivas]

Where is 1729 used?

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

I am not sure we are thinking in the right direction with squares, because in squares + identity elements, we again find both 817 and 1729 satisfied, but it seems impossible to find a magma where non square elements also satisfy 1729 and not 817.

[Shreyas Srinivas]

But that's just going back to square one.

[Shreyas Srinivas]

The square conditions must surely be extraneous

[Terence Tao]

Shreyas Srinivas said:

Where is 1729 used?

Sorry, I was being brief (repeating arguments from earlier in the thread). The argument is as follows:

From 1729 one has $L_{Sx} R_{x} L_x S^2 x = S^2 x$, which we can rearrange as $L_{Sx} R_x R_{S^2 x} x = L_{Sx} R_x x$. Since $L_{Sx}$ is invertible, we conclude $R_x R_{S^2 x} x = R_x x$. If $x$ is a square $x = Sy$, then $R_x$ is also invertible, so we conclude that 817 ($R_{S^2 x} x = x$) holds for square numbers, or equivalently that $Sy \diamond S^3 y = Sy$ for all $y$.

[Terence Tao]

Here is an annoying obstruction:

Theorem. Suppose that a 1729 magma $M$ is such that $SM$ is finite and closed under multiplication. Then 817 holds.

So we will need an infinite base magma if one is to try to build the counterexample starting from the squares.

Proof. Let $x \in M$; our aim is to show that $R_{S^2 x} x = x$. For $a \in SM$, we have $L_{Sa} R_a L_a = 1$ by 1729, hence $R_a^{-1} = L_a L_{Sa}$. So, if we set $y_a := L_a L_{Sa} x = R_a^{-1} x$, it suffices to show that $y_{S^2 x} = x$.

For any $a \in SM$, we have
$a = L_{Sy_a} R_{y_a} L_{y_a} a = L_{Sy_a} (R_a y_a \diamond y_a) = L_{Sy_a} L_x y_a. \quad (1)$
This already shows that the map $a \mapsto L_x y_a$ is injective from $SM$ to $SM$ (since by hypothesis $L_x$ is injective and the bijection $L_{Sy_a}$ preserves the finite set $SM$), hence is also a bijection. In particular there exists $a$ with $L_x y_a = Sx$, hence $y_a = x$ by injectivity of $L_x$. Inserting this back into (1) we obtain $a = S^2 x$, hence $y_{S^2 x} = x$ as required. $\Box$

[Terence Tao]

I think I was finally able to get a greedy construction to work to refute 1729 => 817. The details are en route to the blueprint at equational#866 (EDIT: now landed), but the ideas are as follows.

• The carrier $M$ will be the disjoint union $M = SM \uplus N$ of a set $SM$ of squares and a set $N$ of non-squares.
• For the squares $SM$, I took an infinite abelian group of exponent 4, which already obeys 1729. Because of previous obstructions, this was the simplest choice for $SM$ that was available.
• Next, we select the right multiplication operators $R_a: N\to N$ for $a \in SM$. (It took me a while to realize that this was the component that had to be pinned down first, after fixing $SM$; I spent way too long trying to pin down $L_a$ first.) Here I took the "free" option in which $N$ is the free non-abelian group generated by $e_a, a \in SM$ and $R_a$ is left-multiplication by $e_a$. So there are no relations between any of the $R_a$.
• Because of the 1729 identity $L_{2a} R_a L_a = 1$ for $a \in SM$, we can write all the left-multiplication operators in terms of $L_0$: indeed after some algebra one finds that $L_a = e_a L_0 e_{2a}^{-1}$ (where by abuse of notation $e_a$ denotes left multiplication by $e_a$).
• One now has to select a map $L_0: N \to N$, a squaring map $S: N \to SM$, and a multiplication operation $\diamond': N \times N \to SM$ obeying a certain number of technical axioms. It turns out that these axioms can be simultaneously satisfied by greedily selecting for $L_0, S, \diamond'$ together (I had previously tried to select each separately, but they were coupled together too annoyingly to do so).

There are two technical issues that complicate this greedy analysis beyond that of previous constructions. The first is that the 1729 identity $L_0 R_0 L_0 = 1$ implies that $L_0^2 = e_0^{-1}$. As a consequence, every time one greedily selects $L_0 x = y$, one is forced to also select an infinite number of additional identities $L_0 e_0^n x = e_0^n y$ and $L_0 e_0^n y = e_0^{n-1} x$. But this is a relatively orderly injection of additional identities, and while annoying, does not cause major difficulties.

More tricky is dealing with the implication
$y \diamond' x = z \implies z \diamond' y = L_{Sy}^{-1} x$
that is a rephrasing of 1729, and which means that every time one fills in one entry of the multiplication table, another one also must be entered. In previous constructions there was a periodicity that let one terminate this iteration after a finite number of steps (six, in fact); but now that $L_{Sy}$ is constructed in a complicated fashion, and $S$ itself was also being constructed concurrently with the other data for the magma, I did not see a way to enforce this periodicity. Instead, I had to introduce a new category to the greedy construction, that of a "pending identity" such as $z \diamond' y = L_{Sy}^{-1} x$, which we want to be true, but cannot yet implement because $Sy$ is undefined. So each time a new entry of the multiplication table is defined, one often has to place an identity such as $z \diamond' y = L_{Sy}^{-1} x$ on the "pending" queue, and later when $Sy$ is defined, any relevant pending identities on the queue then have to be incorporated into the multiplication table (which often then causes further pending identities to go on the queue). It's a bit convoluted, but I did not see a better way to achieve this.

[Shreyas Srinivas]

Awesome!! We still want to pursue a more "human-readable" counter-example right?

[Shreyas Srinivas]

@Mauricio Collares : I am referring to the second paragraph of the daily log of Day 47

[Terence Tao]

Certainly simpler constructions are always welcome! In particular they may be easier to formalize. I opened equational#869 to formalize the above argument, but if a simpler construction comes along it would make sense to formalize that instead.

That said, the large number of immunities this implication had suggests that any other construction may be difficult. I already found it challenging to create examples of a 1729 magma in which $S^3$ was not constant, for instance (probably I could do it by iterating the above construction, but I was not able to construct an algebraically simple example).

[Matthew Bolan]

I thought we knew linear models with that property, for example this one

[Terence Tao]

Oh, fair enough. I meant to say a model where $S$ was not surjective, and the iterates $M, SM, S^2 M, \dots$ didn't stabilize until at least the third power $S^3 M$. Though for the particular greedy construction I used, this wouldn't have been an obviously superior base model anyway, the point was it was hard to sustain genuinely non-surjective squaring over more than two iterations.

[Kevin Buzzard]

So you're now "mathematician-finished" but my instinct is not to celebrate until you're "lean-finished", because there may still be a twist in the story :-) Although it might be tedious to formalise the 80(?) or so "conjectures" we all know from experience that people can make mistakes... This is the "perspiration" after the "inspiration" in the old saying.

Congratulations to all, by the way! It's definitely a great milestone in the project.

[Matthew Bolan]

52 conjectures remain to be formalized, stemming from 13 or 14 equations.

[Shreyas Srinivas]

some of these appear non trivial to formalise so I'd say the field is still open for finding simpler counterexamples

[Kevin Buzzard]

Or for finding errors :-)