713, 1289, 1447

Stream: Equational

[Terence Tao]

We are getting close to a milestone: up to duality, we have only two unresolved implications left (1516->255 and 1729->817), one of which may already be resolved (I am wrting up the proof in blueprint). On the other hand we have 61 implications that have informal proofs, but not Lean proofs as yet (and, through duality and transitivity, imply 125 more). Most of these should "just" require human effort to translate the former into the latter, but I wanted to use this thread to focus on a cluster of eight implications that we currently only have computer-generated proofs involving a large greedy algorithm that was verified by a SAT solver (with duality and transitivity, they imply a few more than this, I think they cover 20 of the 190 outstanding implications). More precisely, the refutations are:

1. 713 x = y ◇ (y ◇ ((y ◇ x) ◇ x)) does not imply 817 x = x ◇ ((x ◇ x) ◇ (x ◇ x)), 1426 x = (x ◇ x) ◇ (x ◇ (x ◇ x)), 3862 x ◇ x = (x ◇ (x ◇ x)) ◇ x, or 4065 x ◇ x = ((x ◇ x) ◇ x) ◇ x.
2. 1289 x = y ◇ (((x ◇ y) ◇ y) ◇ y) does not imply 3116 x = (((y ◇ x) ◇ y) ◇ y) ◇ y or 4435 x ◇ (y ◇ x) = (x ◇ y) ◇ x
3. 1447 x = (x ◇ y) ◇ (x ◇ (z ◇ x)) does not imply 1431 x = (x ◇ x) ◇ (y ◇ (x ◇ x)) or 4269 x ◇ (x ◇ x) = x ◇ (y ◇ x)

I'm starting this thread to discuss how to move forward on these implications. Some of them might be attackable by hand, particularly using some of the many new techniques that we have discovered in the last few weeks. Alternatively, there may be ways to use computer assistance to shrink the current proofs to be formalized in the version of Lean we are using, or perform some autotranslation of the ATP aspects. Anyway, look forward to hearing the proposals.

[Shreyas Srinivas]

I am new to practical use of SMT solvers, but they have the ability to construct proofs and I recall that there is a lean4 project for importing the proofs cvc5 produces

[Shreyas Srinivas]

(deleted)

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

I am out-of-the-loop, so there's a very good chance you've done this already, but:
If possible it might be worth inspecting (a finite prefix of) the multiplication table generated by the greedy algorithms. A human might see a clearer pattern in the actual table than in the greedy rulesets that the solvers produced, allowing one to side-step the machine generated proofs and use something more human-comprehensible in the Lean formalization.

[Michael Bucko]

Zoltan A. Kocsis (Z.A.K.) schrieb:

I am out-of-the-loop, so there's a very good chance you've done this already, but:
If possible it might be worth inspecting (a finite prefix of) the multiplication table generated by the greedy algorithms. A human might see a clearer pattern in the actual table than in the greedy rulesets that the solvers produced, allowing one to side-step the machine generated proofs and use something more human-comprehensible in the Lean formalization.

(I've tried this quite a bit, and have never given up on this. One notices patterns, but, from my experience, they often end up being (quite) local, i.e. end up in deadends.)

[Matthew Bolan]

Inspired by the construction for 854, we might consider adding to the greedy algorithm axioms we know to be true of the universal magma. For example, 713 has a 3 element model with no idempotents , so we should be able to add $x\diamond x \not = x$ as an axiom safely. Looking at the ruleset for 713 , it seems that at least 3 of them,

Rule([[0, 0, 1], [0, 1, 1]], [0, 1]),
Rule([[0, 0, 1], [0, 1, 2], [1, 0, 3], [2, 3, 3]], [0, 1]),
Rule([[0, 0, 1], [0, 1, 2], [1, 0, 3], [2, 3, 3]], [0, 1]),

would imply the existence of an idempotent (Provided I understand the format correctly), so perhaps this can simplify the construction.

[Matthew Bolan]

Perhaps we can choose some finite magma $M$ for which many of the rules from the greedy ruleset never have their precondition met, and then greedily build our counterexample $M'$ under the additional condition that we have a homomorphism $f:M' \to M$.

[Matthew Bolan]

Asking for a homomorphism to the 3 element model I mentioned above seems to take care of quite a few of the rules in the 713 ruleset. In particular (provided I understand the format correctly and there are no bugs in my code) I believe the preconditions to

Rule([[0, 0, 1], [1, 0, 2], [3, 1, 0], [3, 2, 0]], [2, 1])
Rule([[0, 0, 1], [0, 1, 2], [1, 0, 2]], [0, 1])
Rule([[0, 0, 1], [0, 1, 1]], [0, 1])
Rule([[0, 1, 2], [2, 0, 2], [2, 1, 0]], [1, 2])
Rule([[0, 1, 2], [0, 2, 1], [2, 1, 0]], [1, 2])
Rule([[0, 1, 2], [0, 2, 3], [1, 3, 0], [1, 4, 2], [2, 4, 1]], [3, 0])
Rule([[0, 1, 1], [0, 2, 3], [3, 1, 2], [3, 2, 0]], [1, 2, 0])
Rule([[0, 0, 1], [1, 0, 2], [1, 1, 0], [2, 2, 0], [3, 1, 2], [3, 3, 2]], [0, 3])
Rule([[0, 0, 1], [0, 1, 2], [1, 0, 3], [2, 3, 3]], [0, 1])
Rule([[0, 0, 1], [0, 2, 3], [1, 1, 0], [1, 2, 1]], [1, 3, 2])
Rule([[0, 0, 1], [1, 1, 0], [1, 2, 1], [2, 2, 0]], [0, 2, 0])
Rule([[0, 0, 1], [0, 1, 2], [1, 0, 3], [3, 3, 0], [3, 4, 3]], [3, 2, 4])

are never met in the 3-element model. This leaves 11 rules in the ruleset, most of which prover9 says must have their precondition met sometimes in any 713 magma, so cannot be evaded in this way. The lone exception is Rule([[0, 0, 1], [0, 2, 3], [3, 2, 1]], [0, 2]), for which I could not quickly find a finite model with

∀x∀y∀z∀w [(x*x!=y)|(x*z!=w)|(w*z!=y)].

nor could prover9 prove no such model exists. Still, 11 rules is around the size of the largest ruleset we currently deal with, so perhaps this is enough?

[Terence Tao]

I guess @Daniel Weber would be the person to properly weigh in on this, but I like this semi-automated approach to prune the ruleset using finite magma examples to eliminate rules with too many preconditions.

[Terence Tao]

It seems like a "free move" in fact. If a greedy approach works, then I think it also works when one also imposes a homomorphism to a given finite magma that already obeys the law (though in some cases one may possibly need some surjectivity type axioms for left and right multiplication etc. on the finite magma to ensure that a homomorphism value can be assigned, though if the rule is forced by the original equation, and the finite magma also obeys that equation, then this shouldn't actually be a problem). By taking products of all the finite magmas one cares about, one can in fact impose as many homomorphisms as one pleases. So this seems like something that it really doesn't hurt to try on all of the unformalized equations. It's even possible that some of the unformalized implications in which the vanilla greedy approach failed to close, begin closing if we also enforce homomorphisms to finite magmas. In particular 1076 (with its 40 attendant implications, or 80 with duality) would be a tempting target for this.

[Matthew Bolan]

I guess the original greedy approach to 1485 you found can also be thought of like this (only there with a relaxed finite magma).

[Terence Tao]

It's a bit obfuscated by the directed graph language for that equation, but I think you are at least morally right here. So one could also imagine imposing homomorphisms to finite "relaxed" magmas, which basically amounts to requiring the magma to be colored with finitely many colors and with certain color combinations forbidden (red times green is not allowed to equal blue, that sort of thing). This sounds like something that is not easily automatable to find, but may be automatable to formalize once the candidate finite relaxed magma is located.

[Terence Tao]

One could try the semi-automated tactic of designing coloring rules to eliminate some unwanted rule in a partial ruleset, asking one or more ATPs whether such a rule is "affordable", and, if so, implementing it and seeing if reduces the complexity of the partial ruleset, and then iterating in a human guided fashion.

[Terence Tao]

It's also possible that the raw size of the ruleset is not necessarily the thing we want to minimize. For instance, with your 713 example, it may be slightly easier to close the argument (or have an ATP figure out how to do so) if one explicitly retains a no idempotence axiom, even if this axiom is implied indirectly from the axioms that there is a homomorphism to a finite model with no idempotents.

[Matthew Bolan]

1447 has a two element model with no idempotents, that I think takes care of 3 of its 11 rules (assuming I understand the format of the rules and my code has no bugs).

1289 has a three element model with no idempotents that I think takes care of 7 of its 27 rules.

There are two more rules for 1289

Rule([[0, 1, 2], [1, 1, 3], [3, 1, 0], [4, 0, 1], [5, 0, 4]], [0, 2, 5])
Rule([[0, 1, 2], [1, 1, 0], [3, 0, 1], [4, 0, 3]], [0, 2, 4])

that might have a chance of being taken care of by asking for a homomorphism to some other magma, but I could not find a suitable one easily.

Applying this trick to 1076 seems difficult. The magmas we map to must not contain any idempotents, but the anti-implication $1076 \not \to 3$ has not yet been formalized, which suggests we don't know any easy 1076-magmas which are idempotent free.

I will now think about how to search for relaxed magmas to map to I suppose.

[Alex Meiburg]

My understanding is that the difficulty is that there's a step where you need to check that a fairly large set of constraints has no solution, and currently this is done by a SAT solver and it would be prohibitively slow to do the same check in Lean (especially without native_decide).

Proposal: it should be possible to export the UNSAT proof from the SAT checker. These are typically "minimal" trees of implications to follow and check, that -- especially when optimized / compressed -- can be verified orders of magnitude faster than the original SAT solving. There's a few different formats, but one, LRAT, has been implemented in the Lean4 core language. It started as its own separate project initially. Assuming you can cajole the SAT solver to output the UNSAT proof, which shouldn't be _too_ difficult, this should be computationally workable.

[Shreyas Srinivas]

A lot of SMT solvers have an automated feature to prune the set of unsatisfiable assumptions with an unsat core.

[Terence Tao]

@Matthew Bolan Fair enough - this certainly indicates that for all known models, all elements are idempotent! One could still hope that one could rerun the automated greedy algorithm for 1076 with the additional hypothesis of no idempotents (which we know is allowable, due to the translation invariant construction) and see if now it closes, but I don't know if the script for doing so is readily available.

[Michael Bucko]

A couple of ideas:

• Letting the LLM adjust the initial TP file in auto mode, i.e. it'd adjust it based on the initial query and then based on its own learning (feedback from Vampire). I made a slightly modified version of https://github.com/riccitensor/vampirellm and run that kind of LLM-assisted search in the loop.
• Graph neural nets for those implications chains (perhaps including the knowledge of multiplication/transformation chains we're using)
• A model trained to find operation tables that satisfy X and refute Y. I guess Vlad mentioned FinSearch could help with getting the operation table data -- but I haven't used that tool yet.

[Shreyas Srinivas]

For the sat solver proofs. I wanted to ask: How long did the final successful runs take?

[Daniel Weber]

Matthew Bolan said:

Perhaps we can choose some finite magma $M$ for which many of the rules from the greedy ruleset never have their precondition met, and then greedily build our counterexample $M'$ under the additional condition that we have a homomorphism $f:M' \to M$.

This would also require adding rules to make sure this homomorphism is preserved when setting new values, wouldn't it? Adding three predicates type0, type1, type2 this can be made to a bunch of rules

[Daniel Weber]

Shreyas Srinivas said:

For the sat solver proofs. I wanted to ask: How long did the final successful runs take?

713: 11.5 seconds (only 7 of the 23 rules require a SAT solver)
1289: a minute and 24 seconds (only 7 of the 27 rules require a SAT solver)
1447: 3.4 seconds (only 2 of the 11 rules require a SAT solver)

[Daniel Weber]

For 1447 there might be a chance it'll succeed without the SAT solver with proper Vampire configuration and enough time :thinking:

[Daniel Weber]

It succeeded :tada: I think I'll need to implement my idea of having each proof in a separate Lean file, as they're quite large. I'll try this for 713 and 1289, although I'm less hopeful

[Matthew Bolan]

Daniel Weber said:

Matthew Bolan said:

Perhaps we can choose some finite magma $M$ for which many of the rules from the greedy ruleset never have their precondition met, and then greedily build our counterexample $M'$ under the additional condition that we have a homomorphism $f:M' \to M$.

This would also require adding rules to make sure this homomorphism is preserved when setting new values, wouldn't it? Adding three predicates type0, type1, type2 this can be made to a bunch of rules

I think that's right, but provided all rules in the old greedy set are consequences of the original law, the new rules should be easily verified to be preserved, even "by hand". So far most of them accomplish many of the same things as assuming no idempotents though, so you should probably try adding a rule to avoid idempotents before anything else.

Which rules specifically require the SAT solver?

[Daniel Weber]

In 713: rules 2, 6, 10, 11, 12, 16, 23
In 1289: rules 1, 2, 5, 17, 22, 24, 26, 27
(one indexed)

[Daniel Weber]

No idempotents means $x^2 \ne x$ for all $x$, right?

[Matthew Bolan]

Yes

[Matthew Bolan]

In 713 it would prevent 23 from ever being needed for example (though I see you have just crossed this off). Actually I only checked this for the homomorphism condition, so unsure about original statement.

[Matthew Bolan]

Also, as Terry suggests, you should try 1076 with the additional assumption of no idempotents.

[Matthew Bolan]

I'm unsurprised to see rule 2 as the holdout in both lists, as this seems to be the original law in each case. Rule 1 Rule([[0, 1, 2], [0, 1, 3]], [2, 3]) being a holdout in 1289 surprises me.

I also notice that rules 26 and 27 for 1289 are the ones I mentioned above, where it might be allowable to assume their preconditions are never met, but I cannot produce a finite model to prove this.

I think the precondition for 26 is the existence of $v,y$ such that $(v\diamond ((y\diamond y)\diamond y))\diamond ((y\diamond y)\diamond y)=y$, and the precondition for 27 is the existence of $u,y$ such that $(u\diamond(y\diamond y))\diamond(y\diamond y)=y.$

[Daniel Weber]

Daniel Weber said:

It succeeded :tada: I think I'll need to implement my idea of having each proof in a separate Lean file, as they're quite large. I'll try this for 713 and 1289, although I'm less hopeful

Hmm, it uses new deduction rules (forward subsumption demodulation, unit resulting resolution, factoring), and I likely won't have time to implement them this week. If anybody wants to experiment with this, the schedule file I'm using is taking from --mode casc but without anything AVATAR related: noav.sch

[Terence Tao]

For 1076, pen and paper calculations suggest that the vanilla greedy algorithm will work if one imposes the axiom $x \diamond (x \diamond y) \neq y$, i.e. if the statements $x \diamond y = z$ and $x \diamond z = y$ cannot both hold.

For 73, I think imposing $x \diamond y \neq y$ will have a similar effect. For 1692, I suspect imposing $x \diamond y \neq x,y$ could let one close.

[Matthew Bolan]

I think I've managed to get a greedy algorithm to close for 1289, by adding the additional constraint that every element is idempotent. A simulation of the algorithm is able to fill out a 50x50 corner of the table with no issues, and I can also find seeds falsifying the outstanding implications, though they are somewhat large.

At each stage I ask for three things:
Law 1. If $((x \diamond y) \diamond y) \diamond y$ is already defined, then $y \diamond (((x \diamond y) \diamond y) \diamond y)$ is also defined and equals $x$.
Law 2. $R_x$ is injective for all $x$ currently in the table.
Law 3. $x\diamond x=x$ for all $x$ currently in the table.

The algorithm is as follows:
If $a \diamond b$ is currently undefined, introduce a new element $c$ and define $a \diamond b = c$ and $c \diamond c = c.$ If furthermore $a = (d \diamond b) \diamond b$ for some d, then also define $b \diamond c = d$ (This last step is well defined by injectivity of $R_b$).

We now check that the three axioms still hold. Law 3 is obvious, law 2 follows since $d \not = c$. For law 1, we first make the observation that $a \not = b$, for otherwise $a \diamond b$ would have been defined. This has the consequence that if $d$ exists, then $d \not = b$, for otherwise $a = (b \diamond b) \diamond b = b.$ In particular, the product $d \diamond c$ remains undefined after running the algorithm once.

We now work by cases on the values of the variables $x,y$ appearing in law 1:
Case 1: $y=c$. In this case, for the product $x \diamond y$ to be defined, we require $x =b$ or $x = c$. In the former case either $b \diamond c$ or $(b \diamond c) \diamond c = d \diamond c$ is not defined. In the latter case, law 1 holds as $c$ is idempotent.
Case 2: $y=b$. For $((x \diamond b) \diamond b) \diamond b$ to be defined now but not have been defined before, we require one of $x= a, (x \diamond b) = a, ((x \diamond b) \diamond b) = a.$ The first two cases are eliminated as $c \diamond b$ is not yet defined. The last case holds as then $d$ exists and equals $x$, so $b \diamond (((x \diamond b) \diamond b) \diamond b) = b \diamond (a \diamond b) = b \diamond c = x.$
Case 3: $y \not = c, y \not = b$. We have introduced no new products with a righthand side other than $c$ or $b$, so if $((x \diamond y) \diamond y) \diamond y$ was undefined before it remains undefined now.

[Terence Tao]

That's great! Hopefully this can be translated into a ruleset that can feed into @Daniel Weber 's existing tooling to automatically convert into a Lean proof. If that works, I can try to do the same for 1076, 73, and 1692, for which a roughly similar approach to the one above (enforcing some natural (and forced) injectivity conditions, and also an additional condition to avoid unwanted edge cases) seems to work.

[Terence Tao]

Actually, let me just go ahead and do this for 73: $x = y \diamond (y \diamond (x \diamond y))$. Note that this forces $R_y$ to be injective.

The three asks are:
Law 1. If $y \diamond (x \diamond y)$ is defined, then $y \diamond (y \diamond (x \diamond y))$ is defined and equal to $x$.
Law 2. $R_y$ is injective for all $y$ currently in the table.
Law 3.  $x \diamond y \neq y$ for all $x,y$ currently in the table. (The reason for this law will be made clearer later.)

I have not yet verified that there are seeds obeying these laws that refute 99, 125, 203, 229, 255, 4380, 4435, but expect this to be straightforward.

Algorithm: If $a \diamond b$ is undefined, set it equal to a new element $c$. If we also have $b = d \diamond a$ for some $d$ (unique by Law 2, and only possible for $a \neq b$ by Law 3), set $a \diamond c = d$.

It is obvious that Laws 2, 3 are preserved. Now we case check Law 1:

Case 1: $x=c$ or $y=c$. Not possible since no left multiplication with $c$ is defined.
Case 2: $x \diamond y = c$. Only possible when $x = a$, $y = b$, but then $y \diamond (x \diamond y)$ is undefined since $y = b \neq a$ if $d$ is defined.
Case 3. $y \diamond (x \diamond y) = c$. Only possible when $y=a$ and $x=d$, and holds in this case.
Case 4: $x, y, x \diamond y, y \diamond (x \diamond y) \neq c$: this case is already covered by the previous seed.

[Matthew Bolan]

I agree with your claim about 1076 as well, I found the 1289 argument after reproving your 1076 result for myself.

[Terence Tao]

In the other hand, I withdraw my claim about "Dupont" 1692 $x = (y \diamond x) \diamond ((y \diamond x) \diamond y)$. There is an annoying consequence of this law: if $a = b \diamond d$, then $a \diamond b = d \diamond (d \diamond a)$. (Proof: $a \diamond (a \diamond b) = (b \diamond d) \diamond ((b \diamond d) \diamond b) = d$, hence $d \diamond (d \diamond a) = (a \diamond (a \diamond b)) \diamond ((a \diamond (a \diamond b)) \diamond a) = a \diamond b$.) So if one tries to greedily ask for $a \diamond b = c$ then one also must ask for $d \diamond (d \diamond a) = c$. In principle this process could iterate and it looks difficult to control with a finite number of laws.

[Terence Tao]

Just for completeness, here is the analysis for 1076: $x = y \diamond ((x \diamond (x\diamond y)) \diamond y)$.
Law 1: If $(x \diamond (x\diamond y)) \diamond y$ is defined, then $y \diamond ((x \diamond (x\diamond y)) \diamond y)$ is defined and equal to $x$.
Law 2: For each $y$, the map $x \mapsto x \diamond (x\diamond y)$ is injective where it is defined.
Law 3: $x \diamond (x\diamond y) \neq y$ for all $x,y$ for which the left-hand side is defined.

There are 40 implications to refute and I will not attempt to build seeds for any of them, but expect that this is routine.

Algorithm: If $a \diamond b$ is undefined, set it equal to a new element $c$. If we also have $a = d \diamond (d \diamond b)$ for some $d$ (necessarily unique by Law 2, and only available for $a \neq b$ by Law 3), we also set $b \diamond c = d$.

It is straightforward to check that Laws 2, 3 are preserved. Case analysis for Law 1:

Case 1: $x$, $y=c$, or $x \diamond (x \diamond y) = c$. Not possible as no left-multiplication with $c$ is defined.
Case 2: $x \diamond y=c$. Only possible if $x=a$, $y=b$, but then $x \diamond (x \diamond y)$ is undefined since $x = a \neq b$ if $d$ is defined.
Case 3: $(x \diamond (x \diamond y)) \diamond y = c$. Then $x=d$, $y=b$, and the claim follows by construction.
Case 4: No term is equal to $c$: this case is covered by the existing seed.

[Terence Tao]

One could perhaps revisit the other outstanding equations 3308, 1526, 917, 1722, 63 not currently claimed to see if there are similarly cheap greedy resolutions available.

[Matthew Bolan]

When I'm home again I think I'm set up to do any needed seed finding tasks automatically.

[Matthew Bolan]

For 1289 the seed

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

has a 4435 failure at (x,y)=(0,1) and a 3116 failure at (2,0).

For law 73 I found

these seeds for the outstanding laws

Failure of Equation99[x = x ◇ ((x ◇ x) ◇ x)] at 1
========
2 2 _ _
_ 0 3 0
_ _ _ _
_ _ _ _
========
Failure of Equation125[x = y ◇ ((y ◇ x) ◇ y)] at 1 0
========
2 0 3 0
_ 2 _ _
_ _ _ _
_ _ _ _
========
Failure of Equation203[x = (x ◇ (x ◇ x)) ◇ x] at 0
========
1 2 0 _
_ _ _ _
3 _ _ 0
_ _ _ _
========
Failure of Equation229[x = (y ◇ (y ◇ x)) ◇ y] at 2 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========
Failure of Equation255[x = ((x ◇ x) ◇ x) ◇ x] at 1
========
2 2 _ _
_ 0 _ _
_ 3 _ _
_ _ _ _
========
Failure of Equation4380[x ◇ (x ◇ x) = (x ◇ x) ◇ x] at 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========
Failure of Equation4435[x ◇ (y ◇ x) = (x ◇ y) ◇ x] at 0 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========

For 1076, I think I found a hole in the argument. In the case where $y=c$ you say this is not possible as no left-multiplication with $c$ is defined. However, the precondition for law 1 is that $(x \diamond (x \diamond y)) \diamond y$ be defined, which can arise for $y=c$, $x=b$ if $b \diamond (b \diamond c) = b \diamond d = b$, even without any left multiplication with $c$ being defined. Unfortunately my own version of the argument does not seem to fare much better. The arguments for 73 and 1289 still seem fine to me though, and unlike my attempts with 1076, I am able to fill out large corners of the multiplication table with them.

[Terence Tao]

Oof, you are right. Trying to fix the 1076 argument by adding more rules and laws seems to create a combinatorial explosion that I don't see how to close. (Now I wonder how the translation invariant construction for 1076 gets around this problem...)

[Terence Tao]

OK, after analyzing @Pace Nielsen's translation invariant construction of 1076 magmas, I see that it can be adapted to a non-translation-invariant greedy construction, but with the 1076 law broken up differently. In particular, one does not add just a single new element at each step, but instead quite a few new elements, so it is unlikely that there will be a cheap way to formalize this from the automated greedy algorithm tooling we have. On the other hand, the removal of the group structure may make this formulation of the argument slightly easier to formalize.

There are just two laws:

Law 1. If $x \diamond (x \diamond y)$ is defined and equal to some $z$, then $y \diamond (z \diamond y)$ is defined and equal to $x$.
Law 2. $x \diamond x$ is not equal to $x$.

Now for the greedy construction:

• Locate an undefined entry $a \diamond b$ in the multiplication table, and set it equal to some new element $c$.
• If $d_i$ are the elements for which $a \diamond d_i = b$, set $c \diamond d_i$ equal to some new element $c'_i$, and also set $d_i \diamond c'_i$ equal to $a$.
• If $d_i \diamond a$ is equal to some $e_i$, set $e_i \diamond c'_i = c''_i$ and $c'_i \diamond c''_i = d_i$, where $c''_i$ is equal to $a$ if $e_i = d_i$, or some new element otherwise.

One can verify that no collisions are caused by this construction (this is why we have to take $c''_i=a$ when $e_i=d_i$), and that Law 2 is preserved.

We need to verify that these constructions preserve Law 1. There are several cases:

• $y=c$. Not possible since there are no right multiplications by $c$ defined.
• $x=c$. Not possible since it forces $y = d_i$, $x \diamond y = c'_i$ for some $i$.
• $y=c'_i$, $x = d_i$. True by construction.
• $y=c'_i$, $x \neq d_i$. This forces $x = e_i \neq d_i$ and $x \diamond y = c''_i$, but then $x \diamond (x \diamond y)$ is undefined.
• $x=c'_i$. Not possible because this forces $x \diamond y = d_i$, and $x \diamond (x \diamond y)$ will be undefined. (Here we use the fact that $e_i=d_i$ can only occur when $d_i \neq a$, by Law 2.)
• $x = c''_i$ is new. Not possible as no left multiplications by $c''_i$ are defined.
• $y=c''_i$ is new. This forces $x = c'_i$ and $x \diamond y = d_i$, but then $x \diamond (x \diamond y)$ is undefined.
• $x$ and $y$ are not new, but $x \diamond y$ is new. This requires $x=a, y=b$, but then $x \diamond (x \diamond y)$ is undefined since right multiplication by $c$ is undefined.
• $x$, $y$, $x \diamond y$ are not new, but $x \diamond (x \diamond y)$ is new. This requires $x=a$, $x \diamond y = b$, hence $y = d_i$ for some $i$. The claim now follows from construction.
• None of $x$, $y$, $x \diamond y$, $x \diamond (x \diamond y)$ are new. This follows from the previous seed.

[Jose Brox]

Terence Tao ha dicho:

One could perhaps revisit the other outstanding equations 3308, 1526, 917, 1722, 63

Regarding 63 (Dupont), I noticed back then that we could add the identity
$xx^2 = yy^2$
seemingly without implying 1692 (Dupond), what imposes more useful restrictions. In particular it implies that there is an element $a$ such that $a^2 = a$ and no other $x$ has $x^2 = a$ or $x^2=x$ (neither can we have $x^2 = y$ and $y^2 = x$ for any two $x,y$). It also implies $xa = x$ and $ax^2 = x$, which in addition to $x^2x = x$, $xx^2 = a$ and $a = x(a(ax))$ seemed to almost determine a single infinite model. Perhaps this idea could be adapted for a simpler greedy algorithm?

[Jose Brox]

Jose Brox ha dicho:

Regarding 63 (Dupont), I noticed back then that we could add the identity
xx2=yy2
seemingly without implying 1692 (Dupond),

I have rechecked it giving Prover9 30 minutes and high resources.

[Terence Tao]

I managed to translate the second Dupont construction in the blueprint into non-translation invariant language, similar to previous constructions in this thread, using @Jose Brox 's observations to make a (slightly) simpler seed, though I found it useful to work with an explicit squaring operation ($x \mapsto 2x$ on the rationals, though any bijection with a single fixed point would have sufficed) for notational reasons. The ruleset is
Law 1. If $x \diamond (x \diamond y)$ is defined, then $y \diamond (x \diamond (x \diamond y))$ is defined and equal to $x$.
Law 2. If $x \diamond y = x \diamond z$ with $y,z$ distinct, then $y \diamond x$ (if defined) is not equal to $z$ or to $z \diamond x$ (if defined).

In order to avoid an unfavorable case later on, we select the following (infinite) seed. Take the carrier ${\mathbf Q}$ and impose the following initial rules for all $x$:
$x \diamond x = 2x; x \diamond 2x = 0; x \diamond 0 = x; 0 \diamond 2x = x; 2x \diamond x = x.$
The constant $0$ here plays the role of $a$ in Jose's observations, and the rules here correspond to Jose's identities. A finite case check reveals that this initial seed obeys Law 1 and Law 2. We will consider seeds that involve this initial seed together with a finite number of additional relations of the form $x \diamond y = z$.

Algorithm: If $a \diamond b$ is undefined (which in particular implies $a \neq 0$ and $b \neq 0, a/2, a, 2a$, due to the choice of initial seed), set it equal to a new element $c$, where "new" means "not used by any of the additional relations beyond the initial seed". We can also assure that $2c$ and $c/2$ are new. If we have $b = a \diamond d$ for any $d$ (and note from the initial seed that $d \neq 0, a$), set $d \diamond c = a$. If for such a $d$, $d \diamond a$ is defined and equal to some $e$, set $c \diamond e = d$ (a single $e$ is associated to at most one $d$ thanks to Law 2, so this is well-defined).

This creates a new partial function. Let's first verify Law 2. Cases in which $x,y \in \{0,c/2,c,2c\}$ are handled by the initial seed, so we can assume that at least one of $x,y$ lies outside this set. The case $x=c$ cannot occur because each $d$ in the law $c \diamond e = d$ is associated to at most one $e$. If $y=c$, then $x = d$ for some $d$ with $b = a \diamond d$, and then by Law 2 and construction $y \diamond x = c \diamond d$ is undefined, so this case is vacuous. If $z=c$ and $x,y \neq c$, then similarly $z \diamond x$ is undefined, and $y \diamond x$ is not equal to $c = z$, so we are ok in this case also.

Now we verify Law 1. There are several cases.

Case 0: $x,y \in \{0,c/2,c,2c\}$. This case is covered by the initial seed, so now we assume going forward that at least one of $x,y$ lies outside this set.
Case 1: $x=c$. Then $y$ is of the form $e$ for one of the additions $c \diamond e = d$, but then $x \diamond (x \diamond y)$ is undefined by Law 2.
Case 2: $y=c$. Then $x$ is of the form $d$ for one of the additions $d \diamond c = a$, and $d \diamond a$ is defined and equal to some $e$, and the claim follows from construction.
Case 3: $x \diamond y = c$. Then $x=a$ and $y=b$. Since $d \neq a$, $x \diamond (x \diamond y)$ is undefined.
Case 4: None of $x, y, x \diamond y$ are equal to $c$. Then this case is covered by the previous seed.

[Terence Tao]

Roughly speaking, it seems that Dupont has a "rigid" portion of the multiplication table, in which the row $x$ and column $y$ are related to each other via the squaring map by relations such as $y = x^2$ or $y = x \diamond x^2$, where there are a lot of constraints and relatively little freedom to fill out the table, but then the rest of the table is quite "non-rigid" and can be filled out greedily.

[Jose Brox]

Terence Tao ha dicho:

I managed to translate the second Dupont construction in the blueprint into non-translation invariant language, similar to previous constructions in this thread, using @Jose Brox 's observations to make a (slightly) simpler seed

Wow, that was fast! :star_struck:

Since you mentioned the rigidity of Dupont related to squaring, I have remembered that there were at least two other "square identities" we could seemingly add to 63 anti 1692, and both of smaller degree than $xx^2 = yy^2$ (a). Paradoxically, they seemed (at least to me) to remove less freedom from the problem, but perhaps you want to have a thought with them while you have it fresh: they are $x = x^2$ (b, all elements are idempotent) and $x^2 = y^2$ (c, all squares are equal). They cannot be joined: (b)+(c) and (b)+(a) imply $x=y$, while (a)+(c)+63 implies 1692.

[Terence Tao]

Oh, option (b) seems to greatly simplify the problem, moving things back to a vanilla greedy algorithm! Here is the new 63 construction:

Law 1. If $x \diamond (x \diamond y)$ is defined, then $y \diamond (x \diamond (x \diamond y))$ is defined and equal to $x$.
Law 2. If $x \diamond y = x \diamond z$ with $y,z$ distinct, then $y \diamond x$ (if defined) is not equal to $z$ or to $z \diamond x$ (if defined).
Law 3: If $x \diamond x$ is defined, it is equal to $x$.
Law 4: If $x \neq y$, then $x \diamond y$ is not equal to $x$.

We start with the traditional finite seed, rather than the infinite seed used previously.

Algorithm: If $a \diamond a$ is undefined, set $a \diamond a = a$. This clearly does not destroy Laws 3 or 4, and because of Law 4, Law 2 will also be retained. Finally, using Law 4, we can check that this addition does not break Law 1.

Now suppose that $a \diamond b$ is undefined with $a \neq b$, then we set $a \diamond b = c$ for some new $c$. If we have $b = a \diamond d$ for any $d$ (and note from Law 3 that we have the crucial inequality $d \neq a$), set $d \diamond c = a$. If for such a $d$, $d \diamond a$ is defined and equal to some $e$, set $c \diamond e = d$ (a single $e$ is associated to at most one $d$ thanks to Law 2, so this is well-defined).

This creates a new partial function. Law 2 is verified as before, but I repeat the text here for convenience. The case $x=c$ cannot occur because each $d$ in the law $c \diamond e = d$ is associated to at most one $e$. If $y=c$, then $x = d$ for some $d$ with $b = a \diamond d$, and then by Law 2 and construction $y \diamond x = c \diamond d$ is undefined, so this case is vacuous. If $z=c$ and $x,y \neq c$, then similarly $z \diamond x$ is undefined, and $y \diamond x$ is not equal to $c = z$, so we are ok in this case also.

Law 3 is clearly unaffected, and it is also straightforward to check that Law 4 is also not invalidated (here it is essential that $d \neq a$).

Now we verify Law 1. This is the same case analysis, but with the contribution of the initial seed removed:

Case 1: $x=c$. Then $y$ is of the form $e$ for one of the additions $c \diamond e = d$, but then $x \diamond (x \diamond y)$ is undefined by Law 2.
Case 2: $y=c$. Then $x$ is of the form $d$ for one of the additions $d \diamond c = a$, and $d \diamond a$ is defined and equal to some $e$, and the claim follows from construction.
Case 3: $x \diamond y = c$. Then $x=a$ and $y=b$. Since $d \neq a$, $x \diamond (x \diamond y)$ is undefined.
Case 4: None of $x, y, x \diamond y$ are equal to $c$. Then this case is covered by the previous seed.

[Bruno Le Floch]

Seeing all this progress using the greedy algorithm on two-variable equations, it seems like there might be a more general lesson that two-variable equations put sufficiently few constraints that greedy algorithms tend to work for falsifying false implications. Should we expect that implication be decidable for pairs of two-variable equations?

[Terence Tao]

I'm not sure how strong a conclusion we can extrapolate from the relatively short equations we have here. The problem we face with the greedy algorithm is to avert the "combinatorial explosion": if we want the ability to greedily extend a multiplication table to obey N rules, then often one has to impose M additional rules on the initial seed in order to prevent a contradiction. If M is less than N, then one can hope to iterate this process and converge to a finite set of rules that is self-propagating and allows the greedy algorithm to work, particularly if one is aggressive about "pruning" the ruleset by imposing some global axioms that eliminate the most problematic edge cases (e.g., ruling out idempotents, if idempotence causes a lot of such edge cases). But if M is greater than N, iterating the greedy algorithm typically creates exponential growth in the number of rules and it becomes harder and harder to hope to close the whole argument.

The longer the law one is trying to satisfy, the more ways a small number of additions to the multiplication table can potentially destroy the law, and so I think for longer laws it becomes more likely that the greedy algorithm passes the combinatorial explosion threshold and ceases to be usable, even if only two variables are involved. So I would doubt that there is a general decidability result for these sorts of equations with arbitrary length. I think a more realistic goal is to develop enough expertise with the greedy method that slightly longer equations (or collections of equations) than currently studied can be attacked with this method, but not to hope for a method that works with a lot of generality.

[Terence Tao]

May as well try to convert the other greedy resolutions of equations into this language. Here is a version of
@Pace Nielsen 's resolution of 3308, $x \diamond y = x \diamond (x \diamond (y \diamond x))$ without using the translation invariant ansatz.

Law 1: If $x \diamond y$ is defined and equal to $z$, and $y \diamond x$ is defined and equal to $w$, then $x \diamond (x \diamond w) = z$ and $y \diamond (y \diamond z) = w$.
Law 2: $x \diamond y$ is never equal to $x$ or $y$.
Law 3: If $x \diamond y$ is defined and equal to $z$, but $y \diamond x$ is undefined, then $y \diamond z$ and $z \diamond y$ are also undefined.
Law 4: If $x \diamond y$, $z \diamond y$ are defined and equal to each other, then $z=x$.
Law 5: Suppose that $x,y,z,w$ are such that $y \neq z$, $x \diamond y$ is defined and equal to $z$, and $w \diamond z$ is defined and equal to $y$. Then $z \diamond w$ (or symmetrically, $y \diamond x$) are defined.

Algorithm: If $a \diamond a$ is undefined, pick new elements $c_0,c_1,\dots,c_7$ and set $a \diamond a = c_0$, $a \diamond c_0 = c_1$, $a \diamond c_1 = c_0$, $c_0 \diamond a = c_2$, $a \diamond c_2 = c_3$, $a \diamond c_3 = c_1$, $c_0 \diamond c_1 = c_4$, $c_0 \diamond c_4 = c_2$, $c_1 \diamond a= c_5$, $a \diamond c_5 = c_6$, $a \diamond c_6 = c_0$, $c_1 \diamond c_0 = c_7$, $c_1 \diamond c_7 = c_5$. One can check that this preserves Laws 1-5.

Now suppose that $a \diamond b$ is undefined for some $a \neq b$. There are two cases. First suppose that $b \diamond a$ is already defined and equal to some $d$. By Law 3, $a \diamond d$ and $d \diamond a$ are currently undefined, and also by Law 2 $d \neq a,b$. By Law 5, if $x \diamond d = a$ for some $x$, then $d \diamond x$ is also defined. Then pick new elements $c_0,c_1,c_2$ and set $a \diamond b = c_0$, $b \diamond c_0 = c_1$, $b \diamond c_1 = d$, $a \diamond d = c_2$, $a \diamond c_2 = c_0$. One can check that these additions preserve Laws 1-5.

Now suppose that $a \diamond b$ and $b \diamond a$ are both undefined with $a \neq b$. Then introduce new elements $c_0,c_1,c_2,c_3$ and define $a \diamond b = c_0$, $b \diamond c_0 = c_1$, $b \diamond c_1 = c_2$, $b \diamond a = c_2$, $a \diamond c_2 = c_3$, $a \diamond c_3 = c_0$. Again, one can check that these additions preserve Laws 1-5.

[Terence Tao]

Translation of the 1526 argument $x = (y \diamond y) \diamond (y \diamond (x \diamond y))$.

Law 1: If $y \diamond (x \diamond y)$ exists, then $(y \diamond y) \diamond (y \diamond (x \diamond y))$ exists and is equal to $x$.
Law 2: If $x \diamond y$, $z \diamond y$ exist and are equal, then $x=z$.
Law 3: If $x \diamond x$ exists, then $(x \diamond x) \diamond (x \diamond (x \diamond x)) = x$ and $((x \diamond x) \diamond (x \diamond x)) \diamond x = x$.

Algorithm: Suppose first that $a \diamond a$ is undefined. Choose two new elements $c_0, c_1$ and set $a \diamond a = c_0$, $a \diamond c_0 = c_1$, $c_0 \diamond c_1 = a$, $c_0 \diamond c_0 = c_0$, $c_0 \diamond a = a$. One can check that this preserves Laws 1, 2, 3.

Now suppose that $a \diamond b$ is undefined for some $a \neq b$. Applying the previous step if necessary, we may assume that $a \diamond a = Sa$ is defined. By Law 3, we have $b \neq Sa$. Choose a new element $c$ and set $a \diamond b = c$; if also $d \diamond a = b$ for some $d$ (which is unique by Law 2), set $Sa \diamond c = d$. One can check that this does not disrupt Law 2 or Law 3. For Law 1, we do the usual case analysis:

Case 1: $x=c$ or $y=c$. Not possible since no left multiplication by $c$ is defined.
Case 2: $x \diamond y = c$. This forces $x=a,y=b$ and $y = Sa$, but this is not possible since $b \neq Sa$.
Case 3: $y \diamond (x \diamond y) = c$. This forces $y=a$ and $x=d$, and the claim follows from construction.

[Terence Tao]

Translation of the 917 argument $x = y \diamond ((y \diamond y) \diamond (x \diamond y))$. Write $Sy = y \diamond y$ (initially this map is only partially defined).

Law 1: If $Sy \diamond (x \diamond y)$ is defined, then $y \diamond (Sy \diamond (x \diamond y))= x$.
Law 2: If $Sx = Sy$, then $x = y$.
Law 3: If $Sx$ is defined ,then $x \diamond S^2 x = x$.
Law 4: If $x \diamond y = z \diamond y$, then $x=z$.
Law 5: If $x \diamond y = z$, then $Sz \neq y$.

Algorithm: First suppose that $a \diamond a$ (i.e., $Sa$) is undefined. Set $a_0 := a$ and pick three new elements $a_1,a_2,a_3$, and extend periodically mod $4$. Set $a_i \diamond a_i = a_{i+1}$ (so $a_i = S^i a_0$) and $a_i \diamond a_{i+2} = a_i$ for all $i$. One can check that this does not disrupt Laws 1, 2, 3, 4, 5.

Now suppose that $a \diamond b$ is undefined for some $b \neq a$. By Law 2, we have $a = S a'$ for at most one $a'$. By Law 4, we have $d \diamond a' = b$ for at most one $d$. Applying the previous construction if necessary, we may assume that $Sd$ is already defined. From Law 5, we then have $a' \neq Sb.$

Let $c_0,c_1,c_2,c_3$ be new elements extended peroidically (in particular, $c_0 \neq Sd$). As before we set $c_i \diamond c_i = c_{i+1}$ and $c_i \diamond c_{i+2} = c_i$ for all $i$, and again this does not disrupt Laws 1,2,3,4,5. Then, we also set $a \diamond b = c_0$, and also $a' \diamond c_0 = d$ if $a', d$ exist.

It is easy to see that these further additions do not disrupt Laws 2,3,4,5. Now we verify Law 1 by the usual case check.

Case 0: $x, y \in \{c_0,c_1,c_2,c_3\}$ or $Sy, x \diamond y\in \{c_0,c_1,c_2,c_3\}$. Then one can easily verify that $x,y,z \in \{c_0,c_1,c_2,c_3\}$ and the claim follows by the previous analysis. Thus henceforth we may assume that neither of the relations $x \diamond y = z$ or $Sy \diamond z = w$ are of the form $c_i \diamond c_i = c_{i+1}$ or $c_i \diamond c_{i+2} = c_i$.
Case 1: $y = c_0$ or $x=c_0$. Not possible because $Sy \diamond (x \diamond y)$ is undefined.
Case 2: $x \diamond y = c_0$. Only possible when $x=a, y=b, Sy = a'$, but this is not possible since $a' \neq Sb$.
Case 3: $Sy \diamond (x \diamond y) = c_0$. Only possible if $y = a'$ and $x = d$, and the claim then follows by construction.
Case 4: None of the terms in $Sy \diamond (x \diamond y)$ equal $c_0$. Then the claim follows from the previous seed.

[Terence Tao]

Equation 1722 argument $Sy \diamond ((x \diamond y) \diamond y) = x$.

Law 1: If $(x \diamond y) \diamond y$ is defined, then $Sy \diamond ((x \diamond y) \diamond y) = x$.
Law 2: If $x \diamond y = z \diamond y$ then $x = z$.
Law 3: If $Sx$ is defined, then $(Sx \diamond x) \diamond x$ is defined.
Law 4: If $x \diamond y = y$, then $Sy$ is defined.

Algorithm: Suppose that $a \diamond a$ is undefined, then by Law 4 we have $d \diamond a \neq a$ for all $d$ with $d \diamond a$ defined. Set $a_0=a$ and find nine new elements $a_1,a_2,a_3,a_4,b_0,b_1,b_2,b_3,b_4$ with the indices extended periodically by setting $a_{i+4} = a_i, b_{i+4} = b_i$ for $i \geq 1$, and define $a_i \diamond a_i = a_{i+1}$ (so $a_i = S^i a$), $a_{i+1} \diamond a_i = b_i$, $b_i \diamond a_i = a_{i+2}$, $a_{i+3} \diamond a_{i+1} = a_{i+1}$, $a_{i+1} \diamond a_{i+2} = a_{i+1}$, $a_{i+1} \diamond b_i = a_i$. A (slightly tedious) case check shows that Laws 1, 2, 3,4 are preserved.

Now suppose that $a \diamond b$ is undefined for some $a \neq b$. By applying the previous construction, we may assume without loss of generality that $Sb$ is defined. By Law 3, $a \neq Sb \diamond b$. By Law 2, we have $d \diamond b = a$ for at most one $d$, which is necessarily different from $Sb$. If such a $d$ exists, we set $Sb \diamond c = d$.

It is routine to check that Laws 2,3,4 are preserved by this. Now we case check Law 1.

Case 1. $x=c$ or $x \diamond y = c$. Not possible since no left multiplication by $c$ is defined.
Case 2. $y=c$. This would force $x = Sb$ and $d = Sb$, but this is not possible since $d$ is different from $Sb$.
Case 3: $(x \diamond y) \diamond y = c$. This forces $x=d$ and $y=b$, and the claim follows from construction.
Case 4: None of the terms in $(x \diamond y) \diamond y$ are equal to $c$. Then the claim follows from the previous seed.

[Terence Tao]

Similar arguments can actually handle 713: $x = y \diamond (y \diamond ((y \diamond x) \diamond x))$.

Law 1: If $(y \diamond x) \diamond x$ is defined, then $y \diamond (y \diamond ((y \diamond x) \diamond x))$ is defined and equal to $x$.
Law 2: $x \diamond y \neq y$ for all $x,y$. [This is similar to the previous strategy of requiring a homomorphism to an order 3 magma that also obeys this law.]
Law 3: If $Sx$ is defined, then so is $Sx \diamond x$.

Algorithm: First suppose that $a \diamond a$ is not defined. Set $a_0 := a$ and select three new elements $a_1,a_2,a_3$. Define $a_0 \diamond a_0 = a_1$, $a_1 \diamond a_0 = a_2$, $a_0 \diamond a_2 = a_3$, $a_0 \diamond a_1 = a_3$, $a_0 \diamond a_3 = a_0$. It is a routine but tedious matter to check that Laws 1,2,3 are preserved by these operations. (The trickiest case is the $x=a_0$ case of Law 1; here we need Law 2 to prevent $y \diamond a_0$ from equalling $a_0$.)

Now suppose that $a \diamond b$ is undefined for some $a \neq b$. Let $d_1,d_2,\dots,d_n$ be all the elements with $d_i \diamond b = a$. Note from Law 3 that none of the $d_i$ can be equal to $b$. Choose a new element $c$, as well as $c_i$ for each $d_i$, and set $a \diamond b = c$, $d_i \diamond c = c_i$, and $d_i \diamond c_i = b$. It is easy to see that this preserves Laws 2,3. For Law 1 ,we do the usual case analysis.

Case 1: $y = c$, $y = c_i$, $y \diamond x = c$, or $y \diamond x = c_i$. This case cannot occur because we have not defined left multiplication with $c$ or $c_i$.
Case 2: $x = c$ or $x = c_i$. Because $d_i \neq b$, it is easy to see that $(y \diamond x) \diamond x$ is not defined for any $x$.
Case 3: $(y \diamond x) \diamond x = c$ or $(y \diamond x) \diamond x = c_i$. This is only possible if $x=b$ and $y = d_j$ for some $j$, and the claim then follows from construction.
Case 4: None of the terms in $(y \diamond x) \diamond x$ are equal to $c$ or $c_i$. This follows from the previous seed.

[Matthew Bolan]

Wow, I'm impressed it works with such minimal axioms. Even law 2 should be true of the universal magma because of the 3 element model I mentioned a while back.

[Matthew Bolan]

In the third paragraph I think you mean Law 3 and not law 2, and I think some of the $d$ are missing their indices.

[Terence Tao]

I'm struggling to make an analogous human-readable greedy algorithm proof of 1447; it's a three-variable equation rather than a two-variable one, and it seems that any new addition $a \diamond b = c$ to the table generates a lot of additional forced entries via "Sudoku". I am frankly somewhat amazed that the automated greedy method of @Daniel Weber was able to (barely) close the argument here. It may be that this one may require a somewhat different approach (for instance, it has some slight similarity with the weak central groupoid law 1485, so maybe some ideas from that theory may be useful.)

[Matthew Bolan]

In a slightly more human readable format, the rules to the automated greedy solution for 1447 are:

If x ◇ y = z, x ◇ y = w then z = w
If x ◇ y = z, x ◇ w = u, v ◇ x = w then z ◇ u = x
If x ◇ x = x, y ◇ x = z then x ◇ z = x
If x ◇ x = y, y ◇ y = y then x = y
If x ◇ y = z, z ◇ z = z, w ◇ x = z then x = z
If x ◇ y = z, w ◇ w = z then x ◇ w = z
If x ◇ y = z, w ◇ w = x then z ◇ w = x
If x ◇ y = y, y ◇ y = z then x ◇ z = y
If x ◇ y = z, y ◇ z = w, u ◇ v = y then u ◇ w = y
If x ◇ y = z, w ◇ z = x then z ◇ z = x
If x ◇ y = z, w ◇ x = z then x ◇ x = z

[Terence Tao]

Thanks! I must say this is a strange ruleset, the first two are clear but none of the others are obvious to me. There seems to be quite a bit of structure here...

[Matthew Bolan]

Rules 3-5 never have their precondition holding in one of the two element examples I shared earlier, so most of the magic must be happening in the last 6 rules. Maybe a worthwhile experiment would be to just implement the algorithm and figure out which rules it uses the most, and then try and use this to guess other safe rules. I can do this eventually, but I really must finish grading before doing anything else substantial for this project.

[Matthew Bolan]

Hopefully Daniel just gets the automated tooling to work for this one though.

[Terence Tao]

Just for fun I worked out some consequences of 1447 that were able to explain the above rules. First introduce a relation: $x \sim y$ if $x = y \diamond z$ for some $z$. This relation is symmetric: if $x \sim y$, then $x = y \diamond z$, then by 1447, $y = (y \diamond z) \diamond (y \diamond (y \diamond y)) = x \diamond (y \diamond Sy)$, so $y \sim x$. We can then simplify 1447 slightly to the law $y \diamond (x \diamond (z \diamond x)) = x$ whenever $x \sim y$.

Next, given $x,y$, the following are equivalent: (a) $y = x \diamond (z \diamond x)$ for some $z$; (b) $x \sim y$ and $x = w \diamond y$ for some $w$; and (c) $Sy = x$. The implication of (c) from (a) is clear from 1447, and (c) clearly implies (b). Finally, if (b) holds, then by 1447 $y = x \diamond (y \diamond (w \diamond y)) = x \diamond (y \diamond x)$, giving the claim.

The law 1447 now becomes $y \diamond w = Sw$ whenever $y \sim Sw$ (equation 4067).

So one could split up 1447 equivalently into three sublaws:
Law 1: We have $(Sx \diamond y) \diamond x = Sx$ for all $x,y$ (equation 4067)
Law 2: If $y = x \diamond z$ for some $z$, then $x = y \diamond w$ for some $w$ (symmetry of $\sim$)
Law 3: We have $S( x \diamond (y \diamond x) ) = x$ for all $x,y$. (Informally: $\sqrt{x} = x (Mx)$.)

I was able to deduce all of the above ruleset from these facts. It suggests a possible alternate route to constructing 1447 solutions, by first selecting a squaring map, then maybe the relation $\sim$, and then finally the multiplication table itself.

[Jose Brox]

Terence Tao ha dicho:

I'm struggling to make an analogous human-readable greedy algorithm proof of 1447; it's a three-variable equation rather than a two-variable one, and it seems that any new addition a⋄b=c to the table generates a lot of additional forced entries via "Sudoku".

For 1447 anti 1431 or anti 4269 we can seemingly assume (30min in Prover9, 999s in both Vampire and Vampire-SAT) that there exists either a left or a right absorbent element ($0*x=0$ or $x*0=0$, but not both). In particular we can have $x = (x*y)*(x*0)$ and $x = (x*0)^2$. Does this help at all?

[Terence Tao]

OK, here is a general recipe for constructing a 1447 magma.

1. Select a surjective map $S:M \to M$ as the candidate squaring map, with the property that $S$, $S^2$, $S^3$ have no fixed points. Thus, every element $x \in M$ has a non-empty set of square roots $\sqrt{x} := \{y: Sy = x \}$ of which is disjoint from both $x$ and $Sx$. As an explicit example, one can take $M$ to be the irrational elements (or non-dyadic rational elements) of the unit circle ${\mathbb R}/{\mathbb Z}$ and $Sx = 2x$, so $\sqrt{x} = \{x/2 \hbox{ mod } 1,(x+1)/2 \hbox{ mod } 1\}$. One can think of $Sx$ as the "parent" of $x$, and the elements of $\sqrt{x}$ as "siblings" to each other, and "children" of $x$.
2. Define $x \diamond y$ to equal $Sx$ if $Sx=Sy$ or $x = Sy$; equal to $Sy$ if $x = S^2 y$; and equal to an arbitrary square root in $\sqrt{x}$ otherwise. Observe that $x \diamond y$ is either the square of $x$ or the a square root of $x$, with the former possibility occurring if and only if $Sx=Sy$ or $x=Sy$ (i.e. $x$ is a parent or sibling of $y$). Also we have $x \diamond x = Sx$, justifying the interpretation of $S$ as a squaring map.

(informally: sibling * sibling = parent; parent * child = grandparent; grandparent * child = parent; and in all other cases, parent * anyone else = one of the children. Here the relation $x \sim y$ was designed to be the relation that $y$ is the parent or a child of $x$, which was the minimal choice available. One is now basically selecting the ansatz "$x \diamond y$ should equal either the parent or child of $x$" - a sort of shifted left-absorptive ansatz - and figuring out which choice to make in order to enforce 1447.)

Verification of 1447: for any $x,y,z$, $x \diamond y$ is either $Sx$ or in $\sqrt{x}$. By construction, $Sx \diamond \sqrt{x} = x$ and $\sqrt{x} \diamond \sqrt{x} = x$, so it suffices to show that $x \diamond (z \diamond x) \in \sqrt{x}$. By construction, we just need to rule out the possibility that $S(z \diamond x) = Sx$ or $S(z \diamond x) = x$. There are four cases:

• If $S(z \diamond x) = Sx$ and $z \diamond x$ was a square root of $z$ then $z = Sx$, but then $S(z \diamond x) = S^3 x \neq Sx$, contradiction.
• If $S(z \diamond x) = Sx$ and $z \diamond x= Sz$ then $Sz = Sx$ or $z = Sx$, so $Sx = S^2 x$ or $S x = S^3 x$, contradiction.
• If $S(z \diamond x) = x$ and $z \diamond x$ was a square root of $z$ then $z=x$, but then $S(z\diamond x) = S^2 x \neq x$, contradiction.
• If $S(z \diamond x) = x$ and $z \diamond x= Sz$ then $Sz = Sx$ or $z = Sx$, but then $x = S^2 x$ or $x = S^3 x$, contradiction.

I think there is more than enough flexibility in this construction to explicitly contradict 1431 or 4269.

[Daniel Weber]

$\lfloor n/2 \rfloor$ has a fixed point at 0

[Terence Tao]

Ugh, good point. Changed the model accordingly.

[Terence Tao]

Opened equational#832 to deal with 1447 specifically, since we have two promising routes to formalization: translating the ATP-generated proof to Lean, or implementing the above explicit construction.

[Bernhard Reinke]

Terence Tao said:

May as well try to convert the other greedy resolutions of equations into this language. Here is a version of
Pace Nielsen 's resolution of 3308, $x \diamond y = x \diamond (x \diamond (y \diamond x))$ without using the translation invariant ansatz.

Law 1: If $x \diamond y$ is defined and equal to $z$, and $y \diamond x$ is defined and equal to $w$, then $x \diamond (x \diamond w) = z$ and $y \diamond (y \diamond z) = w$.
Law 2: $x \diamond y$ is never equal to $x$ or $y$.
Law 3: If $x \diamond y$ is defined and equal to $z$, but $y \diamond x$ is undefined, then $y \diamond z$ and $z \diamond y$ are also undefined.

Algorithm: If $a \diamond a$ is undefined, pick new elements $c_0,c_1$ and set $a \diamond a = c_0$, $a \diamond c_0 = c_1$, $a \diamond c_1 = c_0$. One can check that this preserves Law 1, Law 2, and Law 3.

Now suppose that $a \diamond b$ is undefined for some $a \neq b$. There are two cases. First suppose that $b \diamond a$ is already defined and equal to some $d$. By Law 3, $a \diamond d$ and $d \diamond a$ are currently undefined, and also by Law 2 $d \neq a,b$. Then pick new elements $c_0,c_1,c_2$ and set $a \diamond b = c_0$, $b \diamond c_0 = c_1$, $b \diamond c_1 = d$, $a \diamond d = c_2$, $a \diamond c_2 = c_0$. One can check that these additions preserve Law 1, Law 2, and Law 3.

Now suppose that $a \diamond b$ and $b \diamond a$ are both undefined with $a \neq b$. Then introduce new elements $c_0,c_1,c_2,c_3$ and define $a \diamond b = c_0$, $b \diamond c_0 = c_1$, $b \diamond c_1 = c_2$, $b \diamond a = c_2$, $a \diamond c_2 = c_3$, $a \diamond c_3 = c_0$. Again, one can check that these additions preserve Law 1, Law 2, and Law 3.

I am not sure whether this algorithm preserves all the laws. The first step seems OK, but I think there is an issue in the second step (where $a \diamond b$ is undefined but $b \diamond a = d$). If there is another element $x$ with $x \diamond a = d$, then we run into problems. Can we impose right-cancellation?

[Bernhard Reinke]

Another problem where I don't have an easy answer: what happens in the second step if there is an x with $x \diamond d = a$? Since we define $a \diamond d$ in the extension, we also need to define $d \diamond x$.

[Terence Tao]

Good points. Fortunately, one can simply add two laws that assert that these scenarios don't happen, and check that they are preserved by the construction (hopefully this doesn't make the seeds impossible to construct, but in past practice non-translation invariant seeds are easy to build). I've updated the argument accordingly.

One way to think about it is to create a directed graph by connecting $y \stackrel{x}{\to} z$ whenever $x \diamond y = z$. One needs to impose axioms that this directed graph does not contain multiple edges, loops, or 2-cycles. But this property will be preserved by construction in all three cases (either one is adjoining a 3-cycle involving two novel vertices, a 4-cycle involving three novel vertices, or connecting up the graph to a fully novel 4-cycle, and inno case are loops, multiple edges, or 2-cycles created).

[Bernhard Reinke]

I don't think the first construction preserves Law 5.

[Bernhard Reinke]

$a \diamond c_0 = c_1$, $a \diamond c_1 = c_0$ is bad, or do you want assume that $x \not= w$?

[Bernhard Reinke]

I will try to see what happens with this variant (so $x \diamond y = z, w \diamond z = y \Rightarrow x = w$), should be ok for Case 1

[Matthew Bolan]

I went ahead and found seeds for the other greedy algorithms in this channel that have not yet been formalized through other means.

1289

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

has a 4435 failure at (x,y)=(0,1) and a 3116 failure at (2,0).

73

Failure of Equation99[x = x ◇ ((x ◇ x) ◇ x)] at 1
========
2 2 _ _
_ 0 3 0
_ _ _ _
_ _ _ _
========
Failure of Equation125[x = y ◇ ((y ◇ x) ◇ y)] at 1 0
========
2 0 3 0
_ 2 _ _
_ _ _ _
_ _ _ _
========
Failure of Equation203[x = (x ◇ (x ◇ x)) ◇ x] at 0
========
1 2 0 _
_ _ _ _
3 _ _ 0
_ _ _ _
========
Failure of Equation229[x = (y ◇ (y ◇ x)) ◇ y] at 2 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========
Failure of Equation255[x = ((x ◇ x) ◇ x) ◇ x] at 1
========
2 2 _ _
_ 0 _ _
_ 3 _ _
_ _ _ _
========
Failure of Equation4380[x ◇ (x ◇ x) = (x ◇ x) ◇ x] at 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========
Failure of Equation4435[x ◇ (y ◇ x) = (x ◇ y) ◇ x] at 0 0
========
1 2 0 _
3 _ _ _
_ _ _ _
_ _ _ _
========

63

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

1722

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

solves all remaining implications with x = 0.

713

Failure of Equation817[x = x ◇ ((x ◇ x) ◇ (x ◇ x))] at 0
Failure of Equation1426[x = (x ◇ x) ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation3862[x ◇ x = (x ◇ (x ◇ x)) ◇ x] at 2
Failure of Equation4065[x ◇ x = ((x ◇ x) ◇ x) ◇ x] at 0
==========
1 3 3 0 _
2 0 1 2 3
2 _ 4 _ 0
_ _ _ _ _
_ 2 4 2 1
==========

1076

Failure of Equation3[x = x ◇ x] at 0
Failure of Equation23[x = (x ◇ x) ◇ x] at 0
Failure of Equation99[x = x ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation203[x = (x ◇ (x ◇ x)) ◇ x] at 0
Failure of Equation307[x ◇ x = x ◇ (x ◇ x)] at 0
Failure of Equation375[x ◇ y = (x ◇ x) ◇ y] at 0 3
Failure of Equation1223[x = x ◇ (((x ◇ x) ◇ x) ◇ x)] at 0
Failure of Equation2441[x = (x ◇ ((x ◇ x) ◇ x)) ◇ x] at 0
Failure of Equation3050[x = (((x ◇ x) ◇ x) ◇ x) ◇ x] at 0
Failure of Equation3456[x ◇ x = x ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation3722[x ◇ y = (x ◇ y) ◇ (x ◇ y)] at 0 3
Failure of Equation3915[x ◇ y = (x ◇ (x ◇ x)) ◇ y] at 0 0
Failure of Equation4118[x ◇ y = ((x ◇ x) ◇ x) ◇ y] at 0 3
Failure of Equation4435[x ◇ (y ◇ x) = (x ◇ y) ◇ x] at 0 0
========
1 2 _ 0
1 _ _ 1
3 _ _ _
_ 0 _ _
========
Failure of Equation151[x = (x ◇ x) ◇ (x ◇ x)] at 0
Failure of Equation326[x ◇ y = x ◇ (y ◇ y)] at 1 0
Failure of Equation817[x = x ◇ ((x ◇ x) ◇ (x ◇ x))] at 0
Failure of Equation1629[x = (x ◇ x) ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation2035[x = ((x ◇ x) ◇ x) ◇ (x ◇ x)] at 0
Failure of Equation2644[x = ((x ◇ x) ◇ (x ◇ x)) ◇ x] at 0
Failure of Equation3522[x ◇ y = x ◇ ((y ◇ y) ◇ y)] at 1 0
Failure of Equation3715[x ◇ y = (x ◇ x) ◇ (y ◇ y)] at 0 0
Failure of Equation4470[x ◇ (y ◇ y) = (x ◇ x) ◇ y] at 0 1
======
1 _ 1
1 2 _
2 _ _
======
Failure of Equation8[x = x ◇ (x ◇ x)] at 0
Failure of Equation411[x = x ◇ (x ◇ (x ◇ (x ◇ x)))] at 0
Failure of Equation1426[x = (x ◇ x) ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation2294[x = (y ◇ (x ◇ (x ◇ y))) ◇ y] at 0 1
Failure of Equation3253[x ◇ x = x ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation3862[x ◇ x = (x ◇ (x ◇ x)) ◇ x] at 0
============
1 2 4 0 1 _
_ _ 5 1 0 _
3 _ _ _ 2 0
_ 0 _ _ _ 0
_ 4 0 _ _ _
2 _ _ _ _ _
============
Failure of Equation47[x = x ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation2238[x = (x ◇ (x ◇ (x ◇ x))) ◇ x] at 0
Failure of Equation3319[x ◇ y = x ◇ (y ◇ (y ◇ y))] at 0 0
==========
1 2 4 0 _
_ _ 0 1 _
3 _ _ _ _
_ 0 _ _ _
2 2 _ _ _
==========
Failure of Equation2847[x = ((x ◇ (x ◇ x)) ◇ x) ◇ x] at 0
========
1 2 _ 0
_ _ 0 2
3 _ _ _
1 _ 0 _
========
Failure of Equation359[x ◇ x = (x ◇ x) ◇ x] at 0
========
1 _ 0 1
2 _ 3 _
_ _ _ 0
3 _ _ _
========
Failure of Equation255[x = ((x ◇ x) ◇ x) ◇ x] at 0
Failure of Equation4065[x ◇ x = ((x ◇ x) ◇ x) ◇ x] at 0
======
1 _ 1
2 _ _
2 _ _
======
Failure of Equation1832[x = (x ◇ (x ◇ x)) ◇ (x ◇ x)] at 0
========
1 2 _ 0
_ _ _ 1
3 2 _ _
_ 0 _ _
========
Failure of Equation3659[x ◇ x = (x ◇ x) ◇ (x ◇ x)] at 0
====
1 _
_ 0
====

3308

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

Here is an example for how to interpret one of the tables:
In the tables for 73, we find

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

This corresponds to the partial multiplication $0 \diamond 0 = 2, 0 \diamond 1 = 2, 1 \diamond 1 = 0, 1 \diamond 2 = 3, 1 \diamond 4 = 0$, which should satisfy the laws of the greedy algorithm for 73, while also having $1 \not = 1 \diamond ((1 \diamond 1) \diamond 1)$, meaning it can serve as a seed for the refutation of $73 \to 99$.

[Bernhard Reinke]

Bernhard Reinke said:

I will try to see what happens with this variant (so $x \diamond y = z, w \diamond z = y \Rightarrow x = w$), should be ok for Case 1

Case 1 is ok again, but this is too weak for case 2

[Matthew Bolan]

Does the 1076 construction need seeds? Looks like I missed in on my first pass

[Matthew Bolan]

1076

Failure of Equation3[x = x ◇ x] at 0
Failure of Equation23[x = (x ◇ x) ◇ x] at 0
Failure of Equation99[x = x ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation203[x = (x ◇ (x ◇ x)) ◇ x] at 0
Failure of Equation307[x ◇ x = x ◇ (x ◇ x)] at 0
Failure of Equation375[x ◇ y = (x ◇ x) ◇ y] at 0 3
Failure of Equation1223[x = x ◇ (((x ◇ x) ◇ x) ◇ x)] at 0
Failure of Equation2441[x = (x ◇ ((x ◇ x) ◇ x)) ◇ x] at 0
Failure of Equation3050[x = (((x ◇ x) ◇ x) ◇ x) ◇ x] at 0
Failure of Equation3456[x ◇ x = x ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation3722[x ◇ y = (x ◇ y) ◇ (x ◇ y)] at 0 3
Failure of Equation3915[x ◇ y = (x ◇ (x ◇ x)) ◇ y] at 0 0
Failure of Equation4118[x ◇ y = ((x ◇ x) ◇ x) ◇ y] at 0 3
Failure of Equation4435[x ◇ (y ◇ x) = (x ◇ y) ◇ x] at 0 0
========
1 2 _ 0
1 _ _ 1
3 _ _ _
_ 0 _ _
========
Failure of Equation151[x = (x ◇ x) ◇ (x ◇ x)] at 0
Failure of Equation326[x ◇ y = x ◇ (y ◇ y)] at 1 0
Failure of Equation817[x = x ◇ ((x ◇ x) ◇ (x ◇ x))] at 0
Failure of Equation1629[x = (x ◇ x) ◇ ((x ◇ x) ◇ x)] at 0
Failure of Equation2035[x = ((x ◇ x) ◇ x) ◇ (x ◇ x)] at 0
Failure of Equation2644[x = ((x ◇ x) ◇ (x ◇ x)) ◇ x] at 0
Failure of Equation3522[x ◇ y = x ◇ ((y ◇ y) ◇ y)] at 1 0
Failure of Equation3715[x ◇ y = (x ◇ x) ◇ (y ◇ y)] at 0 0
Failure of Equation4470[x ◇ (y ◇ y) = (x ◇ x) ◇ y] at 0 1
======
1 _ 1
1 2 _
2 _ _
======
Failure of Equation8[x = x ◇ (x ◇ x)] at 0
Failure of Equation411[x = x ◇ (x ◇ (x ◇ (x ◇ x)))] at 0
Failure of Equation1426[x = (x ◇ x) ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation2294[x = (y ◇ (x ◇ (x ◇ y))) ◇ y] at 0 1
Failure of Equation3253[x ◇ x = x ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation3862[x ◇ x = (x ◇ (x ◇ x)) ◇ x] at 0
============
1 2 4 0 1 _
_ _ 5 1 0 _
3 _ _ _ 2 0
_ 0 _ _ _ 0
_ 4 0 _ _ _
2 _ _ _ _ _
============
Failure of Equation47[x = x ◇ (x ◇ (x ◇ x))] at 0
Failure of Equation2238[x = (x ◇ (x ◇ (x ◇ x))) ◇ x] at 0
Failure of Equation3319[x ◇ y = x ◇ (y ◇ (y ◇ y))] at 0 0
==========
1 2 4 0 _
_ _ 0 1 _
3 _ _ _ _
_ 0 _ _ _
2 2 _ _ _
==========
Failure of Equation2847[x = ((x ◇ (x ◇ x)) ◇ x) ◇ x] at 0
========
1 2 _ 0
_ _ 0 2
3 _ _ _
1 _ 0 _
========
Failure of Equation359[x ◇ x = (x ◇ x) ◇ x] at 0
========
1 _ 0 1
2 _ 3 _
_ _ _ 0
3 _ _ _
========
Failure of Equation255[x = ((x ◇ x) ◇ x) ◇ x] at 0
Failure of Equation4065[x ◇ x = ((x ◇ x) ◇ x) ◇ x] at 0
======
1 _ 1
2 _ _
2 _ _
======
Failure of Equation1832[x = (x ◇ (x ◇ x)) ◇ (x ◇ x)] at 0
========
1 2 _ 0
_ _ _ 1
3 2 _ _
_ 0 _ _
========
Failure of Equation3659[x ◇ x = (x ◇ x) ◇ (x ◇ x)] at 0
====
1 _
_ 0
====

[Terence Tao]

Bernhard Reinke said:

Bernhard Reinke said:

I will try to see what happens with this variant (so $x \diamond y = z, w \diamond z = y \Rightarrow x = w$), should be ok for Case 1

Case 1 is ok again, but this is too weak for case 2

OK, I think I can contain the failure of Law 5 by extending the construction in the first case significantly to add six more elements. A lot less elegant now but hopefully this will work. Text updated accordingly.

[Matthew Bolan]

I think this is a seed which works with the new 3308 greedy laws:

3308

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

[Matthew Bolan]

So with that I think I've found seeds for all greedy algorithms for outstanding implications. Let me know if I missed one.

[Matthew Bolan]

What is the status of 879 and 1692? Looking at Conjectures.lean , 879, 1692, 1323, 1898 , 1447, 1729, 1516 are the equations with outstanding implications that don't have greedy algorithms of this type. 1323, 1898, 1729, 1516 took specialized constructions to resolve at all, and so are unlikely to have an easy reformulation. The greedy approach for 1447 stalled, but we know an easyish construction for the outstanding anti-implications (perhaps Conjectures.lean should be updated to reflect this and other advancements, someone who is only reading the github wouldn't know about the various alternate proofs in this channel). This leaves 879 and 1692, for which the only known proofs seem to be translation invariant greedy constructions. I'm willing to try to convert their arguments into normal greedy constructions, but I see that people may already be working on their formalization.

[Terence Tao]

879 is being worked on by @Amir Livne Bar-on at https://github.com/teorth/equational_theories/pull/830 and seems to be nearing completion. 1692 was claimed by @Aaron Hill on Oct 18, perhaps he can give an update?

I'll update Conjectures.lean now.

[Aaron Hill]

I'm making progress on formailizing the pdf for 1692, but it's been slower than I had hoped. I'm currently partway through Lemma 2.3. I can post my WIP code if that would be helpful

[Terence Tao]

I guess the question is whether you think the current proof is feasible to be formalized as is, or whether some simplification to the theoretical argument would be helpful. But since you are halfway through it, perhaps any major changes to the argument would actually make things harder to formalize.

[Matthew Bolan]

Perhaps you are still updating Conjectures.lean, but 1289 and 713 (of large greedy fame) also have alternate proofs, here and here.

[Matthew Bolan]

You also found an argument for 63 here which I believe is distinct from the two already in the blueprint.

[Bernhard Reinke]

Terence Tao said:

Bernhard Reinke said:

Bernhard Reinke said:

I will try to see what happens with this variant (so $x \diamond y = z, w \diamond z = y \Rightarrow x = w$), should be ok for Case 1

Case 1 is ok again, but this is too weak for case 2

OK, I think I can contain the failure of Law 5 by extending the construction in the first case significantly to add six more elements. A lot less elegant now but hopefully this will work. Text updated accordingly.

I think there were some definitions missing. I added $c_1 \diamond c_7 = c_5$ and $c_0 \diamond c_7 = c_1$, but now $c_7 \diamond c_0$ and $c_4 \diamond c_1$ need to be defined by law 3. At the moment I am finding this via trying to prove this in Lean with aesop, but my proof already becomes quite slow to check. Maybe it makes sense to verify the algorithm first with an ATP such as vampire and then see whether one can convert the vampire proof to an Lean proof as in the greedy algorithm by @Daniel Weber? Would it be possible to extend the language of the greedy algorithm that we can phrase the Laws as "rules" for a variant of the greedy algorithm? Here I am more interested in the verification part, I don't think we can easily extend the greedy algorithm to laws that contain existence statements.

[Matthew Bolan]

I have at least implemented and run for a good while the algorithms for 1289 and 73, which are pretty simple compared to the one you're trying.

[Terence Tao]

@Bernhard Reinke Could you explain the issue with the current argument in more detail? Right now the requirement $c_1 \diamond c_7 = c_5$ is already required, but $c_0 \diamond c_7 = c_1$ is not required, and I also don't see why $c_7 \diamond c_0$ or $c_4 \diamond c_1$ would need to be defined.

[Bernhard Reinke]

I am interpreting Law 1 in the sense that if $x \diamond y$ and $y \diamond x$ are defined, so are $x \diamond (y \diamond x)$ and $x \diamond (x \diamond (y \diamond x))$ and in fact $x \diamond (x \diamond (y \diamond x)) = x \diamond y$. In that case $c_0 \diamond c_1$ and $c_1 \diamond c_0$ are defined, so we need some $d$ with $d = c_0 \diamond (c_1 \diamond c_0) = c_0 \diamond c_7$ and $c_4 = c_0 \diamond d$. I guess one could add a new variable, but $c_0 \diamond c_7 = c_1$ seemed sensible. Maybe one can close this up another way? Similarly, $c_1 \diamond c_4$ needs to be defined.

Or do you mean something else with law 1?

[Terence Tao]

Oh, I see now. This can be closed up by introducing two new variables $c_8,c_9$ and setting $c_1 \diamond c_4 = c_8$, $c_1 \diamond c_8 = c_7$, $c_0 \diamond c_7 = c_9$, $c_0 \diamond c_9 = c_4$. I checked by hand that this closes (I think the only pairs $x,y$ for which $x \diamond y, y \diamond x$ are both defined now are $\{x,y\} = \{a\}, \{c_0,a\}, \{c_1,a\}, \{c_0,c_1\}$, and all the Law 1 invocations should now be resolved without triggering any Law 3 violations), but I can see why this would be tedious for Lean to resolve. It may possibly help to observe that the the only rules $x \diamond y = z$ being imposed here are when $x \in \{a,c_0,c_1\}$, which may cut down on the case analysis. In particular, Law 1 is only triggered when $x,y \in \{a,c_0,c_1\}$, and Law 3 is only problematic when $x \in \{a,c_0,c_1\}$ and at least one of $y,z$ also lie in $\{a,c_0,c_1\}$. Law 4 can only be triggered when $x,z \in \{a,c_0,c_1\}$, and Law 5 can only be triggered when $x,w \in \{a,c_0,c_1\}$.

[Andrés Goens]

Terence Tao said:

OK, here is a general recipe for constructing a 1447 magma.

1. Select a surjective map $S:M \to M$ as the candidate squaring map, with the property that $S$, $S^2$, $S^3$ have no fixed points. Thus, every element $x \in M$ has a non-empty set of square roots $\sqrt{x} := \{y: Sy = x \}$ of which is disjoint from both $x$ and $Sx$. As an explicit example, one can take $M$ to be the irrational elements (or non-dyadic rational elements) of the unit circle ${\mathbb R}/{\mathbb Z}$ and $Sx = 2x$, so $\sqrt{x} = \{x/2 \hbox{ mod } 1,(x+1)/2 \hbox{ mod } 1\}$. One can think of $Sx$ as the "parent" of $x$, and the elements of $\sqrt{x}$ as "siblings" to each other, and "children" of $x$.
2. Define $x \diamond y$ to equal $Sx$ if $Sx=Sy$ or $x = Sy$; equal to $Sy$ if $x = S^2 y$; and equal to an arbitrary square root in $\sqrt{x}$ otherwise. Observe that $x \diamond y$ is either the square of $x$ or the a square root of $x$, with the former possibility occurring if and only if $Sx=Sy$ or $x=Sy$ (i.e. $x$ is a parent or sibling of $y$). Also we have $x \diamond x = Sx$, justifying the interpretation of $S$ as a squaring map.

(informally: sibling * sibling = parent; parent * child = grandparent; grandparent * child = parent; and in all other cases, parent * anyone else = one of the children. Here the relation $x \sim y$ was designed to be the relation that $y$ is the parent or a child of $x$, which was the minimal choice available. One is now basically selecting the ansatz "$x \diamond y$ should equal either the parent or child of $x$" - a sort of shifted left-absorptive ansatz - and figuring out which choice to make in order to enforce 1447.)

Verification of 1447: for any $x,y,z$, $x \diamond y$ is either $Sx$ or in $\sqrt{x}$. By construction, $Sx \diamond \sqrt{x} = x$ and $\sqrt{x} \diamond \sqrt{x} = x$, so it suffices to show that $x \diamond (z \diamond x) \in \sqrt{x}$. By construction, we just need to rule out the possibility that $S(z \diamond x) = Sx$ or $S(z \diamond x) = x$. There are four cases:

• If $S(z \diamond x) = Sx$ and $z \diamond x$ was a square root of $z$ then $z = Sx$, but then $S(z \diamond x) = S^3 x \neq Sx$, contradiction.
• If $S(z \diamond x) = Sx$ and $z \diamond x= Sz$ then $Sz = Sx$ or $z = Sx$, so $Sx = S^2 x$ or $S x = S^3 x$, contradiction.
• If $S(z \diamond x) = x$ and $z \diamond x$ was a square root of $z$ then $z=x$, but then $S(z\diamond x) = S^2 x \neq x$, contradiction.
• If $S(z \diamond x) = x$ and $z \diamond x= Sz$ then $Sz = Sx$ or $z = Sx$, but then $x = S^2 x$ or $x = S^3 x$, contradiction.

I think there is more than enough flexibility in this construction to explicitly contradict 1431 or 4269.

I started mechanizing this construction (in fact, I finished the general construction) in equational#892, but realized that I don't quite grok the reasoning why it would refute 1431 or 4269. I think the S you suggest there on the irrational elements of the unit circle $\R/\Z$ would be bijective, right (not just surjective)? Is there any indicuation that 1431 (x = (x ◇ x) ◇ (y ◇ (x ◇ x))) or 4269 ( x ◇ (x ◇ x) = x ◇ (y ◇ x)) would not hold for that example? or why do we need the quotient over $\Z$)?

I don't want to build that concrete example and only then realize that it doesn't work :sweat_smile:

[Matthew Bolan]

That S would be 2-to-1, it sends both $x$ and $x + \frac{1}{2}$ to $2x$. I believe I have worked through the details and decided it works.

[Andrés Goens]

ahh, right, that makes sense! do you mind sharing what pairs of x and y you used for working out the details on 1431 and 4269?

[Matthew Bolan]

So the rule with carrier $(\mathbb R \setminus \mathbb Q) / \mathbb Z$ and squaring map $x \mapsto 2x$ is

$x \diamond y = \begin{cases} 2x & \text{if } 2x = 2y \text{ or } x = 2y\\ 2y & \text{if } x = 4y \\ \text{An element of our choosing of } \{\frac 1 2 x, \frac 1 2 x + \frac 1 2\} & \text{otherwise} \end {cases}.$

For 4269, x ◇ (x ◇ x) = x ◇ (y ◇ x), as an example take $x,y$ to be $\sqrt 2, \sqrt 3$ (we just need these to be irrational and unrelated enough so the first two cases don't trigger), and suppose we decide $\sqrt 3 \diamond \sqrt 2 = \frac {\sqrt 3}{2}$. Now the lefthand side becomes $\sqrt 2 \diamond 2\sqrt 2$ and the righthand side becomes $\sqrt 2 \diamond \frac 1 2 \sqrt 3$. We are now free to choose the righthand side to disagree with the lefthand side. Specifically, we can win by declaring $\sqrt 2 \diamond 2\sqrt 2 = \frac {\sqrt 2 } 2, \sqrt 3 \diamond \sqrt 2 = \frac {\sqrt 3}{2}, \sqrt 2 \diamond \frac {\sqrt 3}{2} = \frac {\sqrt 2 } 2 + \frac 1 2$

For 1431 things are similar. Declare $\sqrt 3 \diamond 2\sqrt 2 = \frac {\sqrt 3}{2}$ and $2\sqrt 2 \diamond \frac {\sqrt 3}{2} = \sqrt 2 + \frac 1 2.$

[Terence Tao]

If it is inconvenient to work with irrational numbers, an alternative choice of carrier is $M = \{ \frac{a}{p 2^n} \hbox{ mod } 1: a \neq 0 \hbox{ mod } p; n \geq 0 \}$ for a suitably large prime $p$ (I think $p=11$ can work, and one can take the analogues of $\sqrt{2}, \sqrt{3}$ to be $1/11$, $-1/11$).

[Matthew Bolan]

I think the map $S: \mathbb Z^+ \to \mathbb Z^+$ given by
$S(n) = \begin{cases} 8 & \text{if } n=1 \\ \lfloor \frac n 2 \rfloor & \text{otherwise}\end {cases}$
should also work as a squaring map (8 is just to be large enough to avoid any fixed points in $S, S^2, S^3$).

[Terence Tao]

With that model, if one takes $x \diamond y$ to equal $Sx$ if $Sx = Sy$ or $x = Sy$, $Sy$ if $x = S^2 y$, and in other cases $2x$ if $y$ is even and $2x+1$ if $y$ is odd, one should be able to get quite explicit counterexamples here (I didn't perform the calculation though), without needing to make any arbitrary choices.

[Matthew Bolan]

$x = 1$ and $y = 3$ should work to falsify both (after I corrected my silly choice of 4 to be 8).

[Andrés Goens]

thanks! that went through much easier! It's suprisingly hard to get Lean to accept stuff like a * 2 * 1/2 = a, if a is in something like $( \mathbb R \setminus \mathbb Q) / \mathbb Z$ :sweat_smile:

[Kevin Buzzard]

It's not even meaningful, right? This is one of my favourite questions for tripping up undergraduates who've just learnt about vector spaces: "Why isn't $\mathbb{R}/\mathbb{Z}$ a real vector space?". At first glance it looks like all the axioms are satisfied.

[Andrés Goens]

It's a bit sloppy to write it like that, I agree, that's why Lean was giving me a hard time. I meant that the function $a \mapsto a * 2$ is well-defined on $\mathbb R \setminus \mathbb Q$ and if I compose it with the embedding into the quotient then its inverse is what I get by doing the same speel on $a \mapsto a/2$, I think I got that stated in Lean but with some many casts I was happy to go over to the positive integers instead where I had omega and computable stuff that works with rfl

[Matthew Bolan]

For equation 1722 I am nervous about the proof of law 2 continuing to hold after the extension in the $a \diamond a$ case. We define $a_2 \diamond a = a$ in the extension, so for law 2 to continue to hold there cannot have already existed an element $d$ with $d \diamond a = a$, but I see nothing preventing this.

[Terence Tao]

Matthew Bolan said:

For equation 1722 I am nervous about the proof of law 2 continuing to hold after the extension in the $a \diamond a$ case. We define $a_2 \diamond a = a$ in the extension, so for law 2 to continue to hold there cannot have already existed an element $d$ with $d \diamond a = a$, but I see nothing preventing this.

Good catch! I think I can fix it by only being periodic starting from the $1$ index rather than the $0$ index, thus $a_{i+4} = a_i$ for $i \geq 1$ but $a_4 \neq a_0$, and requiring $a_{i+3} \diamond a_{i+1} = a_{i+1}$ rather than $a_{i+2} \diamond a_i = a_i$, so that we don't create a potential collision with $d \diamond a = a$. I've adjusted the text accordingly.

[Matthew Bolan]

I also noticed that the case $x \diamond (x \diamond y) = c$ is missing in the current write-up for 63, but this should hold by construction.

[Matthew Bolan]

I'll go over 1722 again tomorrow. I'm definitely at the point where I can add as much detail as is desired to the blueprint for most of these equations. I'm a little further from any kind of unifying understanding of them that could save us a lot of time (though maybe all these complicated square cases could be dealt with somehow - you're essentially gluing on some other partial magma each time that needs to satisfy some special conditions at the site of the suture), but I definitely can get them all to at least use the same format.

[Terence Tao]

The idea of formalizing the notion of gluing together two partial magmas is potentially promising as a simplifying notion.

[Bernhard Reinke]

Terence Tao said:

Oh, I see now. This can be closed up by introducing two new variables $c_8,c_9$ and setting $c_1 \diamond c_4 = c_8$, $c_1 \diamond c_8 = c_7$, $c_0 \diamond c_7 = c_9$, $c_0 \diamond c_9 = c_4$. I checked by hand that this closes (I think the only pairs $x,y$ for which $x \diamond y, y \diamond x$ are both defined now are $\{x,y\} = \{a\}, \{c_0,a\}, \{c_1,a\}, \{c_0,c_1\}$, and all the Law 1 invocations should now be resolved without triggering any Law 3 violations), but I can see why this would be tedious for Lean to resolve. It may possibly help to observe that the the only rules $x \diamond y = z$ being imposed here are when $x \in \{a,c_0,c_1\}$, which may cut down on the case analysis. In particular, Law 1 is only triggered when $x,y \in \{a,c_0,c_1\}$, and Law 3 is only problematic when $x \in \{a,c_0,c_1\}$ and at least one of $y,z$ also lie in $\{a,c_0,c_1\}$. Law 4 can only be triggered when $x,z \in \{a,c_0,c_1\}$, and Law 5 can only be triggered when $x,w \in \{a,c_0,c_1\}$.

I managed to show that the current version of the laws are satisfied under the first two extension rules, but if we consider the case 3 with $a \diamond b$ and $b \diamond a$ undefined, but if $a = x \diamond b$ for some $x$, then law3 specifies that we also have to define $b \diamond x$.

[Bernhard Reinke]

Ah, I think we do a reduction to case 2 in this setting; we simply run case 2 for x and b instead

[Bernhard Reinke]

Ok, I am done now, see equational#906

[Terence Tao]

Thanks for sorting out the bugs! Hopefully the remaining arguments of this type are not as problematic. I’m grateful to @Matthew Bolan for volunteering to go through the arguments and write them up properly!

I’ll add a note to the (still unwritten) greedy section of the paper that these types of arguments particularly benefit from automation and formalization due to all the crucially important case analysis of edge cases that are often not apparent from one’s intuition about the algorithm

[Matthew Bolan]

I think 3308 was one of the hardest of these seven, 1289, 73, and 713 are all much less complicated. Hopefully the others are not too bad (and I'm glad I now don't need to write up 3308 properly).

[Terence Tao]

Wow, the proof of 3308 is pretty formidable. I guess short of developing a tactic, or an abstract class of "partial solutions" of various types, it's not so easy to create a general purpose theorem to do things like push a partial solution on ℕ ⊕ Fresh back to ℕ, but hopefully it should be much easier to adapt this code to a new implication than to build it from scratch. I do like the idea of establishing laws for these fixed size partial solutions that we then "surgically graft" onto our current partial solution, this at least makes things a little bit more modular.

[Terence Tao]

Perhaps one can formalize an abstract greedy theorem along the following lines? If there is some predicate OK for PreExtension (α : Type) := α → α → Set α that obeys the following hypotheses:

1. If E: PreExtension α is finitely supported and E.OK, and a b: α, then there exists a finitely supported extension E': PreExtension (α ⊕ Fresh) withE'.OK, for which E' a b is non-empty.
2. The OK property is preserved under equivalences.

Then on a countably infinite carrier α, every finitely supported E: PreExtension αwith E.OK generates an infinite sequence of extensions E n: PreExtension α such that for any a b: α, (E n) a b is non-empty for sufficiently large n, that is to say the direct limit of the E n is total (at which point verifying the original law for that limit should be straightforward, even if other components of the OK property fail in the limit).

In principle, all the other arguments then come down to "just" defining an OK predicate and a starting seed E, and verifying the above hypotheses (and showing that the seed refutes whatever we want to refute).

[EDIT: see Theorem 5.10 of the paper draft for one possible proposal in this direction.]

[Matthew Bolan]

I'm still nervous about 1722. If there exists an element $d$ with $d\diamond a = a$, and $a \diamond a$ is undefined, after the extension we have $(a \diamond a) \diamond ((d \diamond a ) \diamond a) = (a \diamond a) \diamond (a \diamond a) = a_1 \diamond a_1 = a_2 \not = d.$ Perhaps we need some condition of the form "If there exists a $d$ with $d\diamond a = a$ then $a \diamond a$ is defined".

[Terence Tao]

You're right, but I think your suggested fix also works. I've updated the text accordingly.

If nothing else, this shows that it was the right call to review these arguments and transfer them to the blueprint.

[Matthew Bolan]

1722 is the only one giving me trouble in this way, the others have gone through smoothly for the most part.

[Matthew Bolan]

I might need to find new seeds for 1722 given the new law.

[Matthew Bolan]

Oh it actually looks like the current 1722 seed is still fine.

[Matthew Bolan]

The proposed fix also should address my first complaint about 1722 as well, so maybe we could revert to the initial way of extending, but I don't really see a reason to.

[Terence Tao]

I'll leave it to your discretion how to write up the 1722 argument in the blueprint, it is meant to supersede the Zulip version of the argument and so does not need to be 100% compatible with it. Basically, whatever exposition makes this group of arguments the easiest to formalize should be the one we should go with.

[Matthew Bolan]

The current version has the nice property that in the square case we don't define any products $x \diamond y$ where $x$ is old and $y$ is fresh, which simplifies the cases somewhat. I think I'm finally convinced by the current 1722 construction.

[Matthew Bolan]

Very happy to see 1722 has been formalized!

[Terence Tao]

And now 1076 too! Great work @Bernhard Reinke !

But it seems that the refutations of 1076 -> 614, 4380 are missing (leading to a temporary blip in the dashboard). @Matthew Bolan , could you run your seed finder algorithm to find seeds for these two implications also? They don't seem to be covered by your previous list.

[Matthew Bolan]

Yes, 614 was a copy pasting error I am reasonably sure, it is covered by

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

which was the sixth table on my original list.

[Shreyas Srinivas]

@Matthew Bolan : as part of this refactoring, could we implement the seed producing algorithm in lean?

[Matthew Bolan]

No way.

[Shreyas Srinivas]

Why?

[Terence Tao]

Perhaps one could formalize a seed _verification_ algorithm in Lean though. (Though it seems simp does an adequate job already).

[Shreyas Srinivas]

To clarify, I am perfectly happy to use the seeds as provided by you or obtained from a partial def using Lean's PL side stuff

[Matthew Bolan]

Currently my seedfinder requires ATP as a key step, those seeds are not small and we need to be able to handle some strange laws. I'm not so familiar with lean or the inner workings of something like Mace4/Vampire, so I should not have spoken so definitively, but to make this thing and formalize that it works is to basically make some form of formalized ATP. That might already exist, in which case it might be possible, but I sort of suspect that if it existed then it would have been used for the small finite counterexamples in lieu of the python scripts I've seen used in this project.

In the absence of that existing, it is probably completely acceptable to have the seeds generated by ATP, and only verified in lean as Terry suggests. This is essentially what we are doing now, and could definitely be made very automatic. However with only 6 equations left, only 3 of which have seeds of this type, I think it wouldn't be worth the effort.

[Bernhard Reinke]

I thought a bit about a possible general seed_verification_algorithm, I think it is easier to do this for laws instead of equations. I think it makes sense to talk about a "partial magma" given by a finite list of equations and have a decidable predicate whether the partial magma refutes a law, such that if a partial magma extends to an actual magma, the refutation persists. But I opted for the simp version for simplicity.

[Bernhard Reinke]

1076 was by far the biggest example, so I made sure that I can use "simp" without having to look myself at the seeds, but work directly with the output of Matthew. If someone wants to play around with syntax metaprogramming, one can try to use the compact version of the seeds, I just parsed them with a simple python script to get back the list form.

[Vlad Tsyrklevich]

No opinion about formalizing the seedfinder, but it would be nice to upstream the current version as I believe it's not currently in the repo?

[Matthew Bolan]

I can try and clean it up and add it to the repo later this week. It has gotten less and less sophisticated as I've gotten better with using ATP to do everything for me.

[Matthew Bolan]

I identified why those two laws were not listed among my seeds. For 1076 I had added at the last minute some lazy code to reduce the number of seeds used for all the laws as much as possible, and this code had a stupid bug in how it was printing the laws satisfied by each magma, which caused some laws that I had in fact found seeds for to simply not be printed.

[Matthew Bolan]

I'll check that the others are not affected, but they should not be.

[Shreyas Srinivas]

We don't necessarily need to formalise its properties right away. Even having the seedfinder code as lean functions would be a good start

[Shreyas Srinivas]

I can foresee a tactic pipeline where a seedfinder tactic produces a seed, by making calls to ATPs as necessary, an augment tactic that takes a next relation and so on.

[Matthew Bolan]

I don't know a lick of lean, so that would probably take me a while. The tactic pipeline sounds possible in principle though.

[Matthew Bolan]

But again, we really only have 3 laws left with this method (and the outside possibility that one of the other laws gets a resolution of this type), all of which have seeds found for them. I figure if future iterations of this project really need something like you describe they can make it.

[Shreyas Srinivas]

For me this is an exercise in distilling and modularising the method.

[Shreyas Srinivas]

And the proofs

[Matthew Bolan]

Well, I'll definitely try and get my code cleaned up and in the repo, and then you can enjoy your exercise.