Austin pairs

Stream: Equational

[Vlad Tsyrklevich]

I'm able to generate ~75 finite implications out of 718 _finite_ unknowns (modulo equivalence, but not duality) on a local branch. I'm using a very simple method to bruteforce generalize the 206=>1648 and 3994=>3588 theorems so I can capture both of those results, and I'm sure that I'm missing some cases.

One interesting observation that I didn't realize until looking at the equation explorer just now is that 3588 and 3994 are duals, and therefore unsurprisingly 3588 also implies 3994 in the finite domain, so they are actually a (finite) equivalence class. 1113/2534 is another dual of this type. Here's a graph (zoom on the right).

[Daniel Weber]

A potential way to automatically prove these implications is to use Vampire, and for a bunch of a functions add the assumption $\text{injective}(f) \leftrightarrow \text{surjective}(f)$, I can try to do that

[Daniel Weber]

Is there some kind of completeness/incompleteness for finite implications? Wikipedia's article on finite model theory says that Godel's completeness theorem fails here, but I don't know if that's already the case for the kinds of implications we're considering

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

@Daniel Weber Trakhtenbrot's theorem is a rather strong obstacle: you won't find a complete logic for finite structures, but even finding a reasonably good logic for finite-ish structures is a difficult open problem in proof theory. E.g. if you formulated the algebraic theory of lattices in such a logic, the logic should provide a proof of existence of a maximal element. If you formulated the theory of integral domains, it should provide a proof of existence of multiplicative inverses. We have no good way of getting something like that.

[Michael Bucko]

Daniel Weber schrieb:

A potential way to automatically prove these implications is to use Vampire, and for a bunch of a functions add the assumption $\text{injective}(f) \leftrightarrow \text{surjective}(f)$, I can try to do that

Daniel, could you please somehow share those snippets / screenshots, or document how you're working with Vampire? That'd be very helpful.

[Daniel Weber]

Michael Bucko said:

Daniel Weber schrieb:

A potential way to automatically prove these implications is to use Vampire, and for a bunch of a functions add the assumption $\text{injective}(f) \leftrightarrow \text{surjective}(f)$, I can try to do that

Daniel, could you please somehow share those snippets / screenshots, or document how you're working with Vampire? That'd be very helpful.

I haven't done this yet, as there are many such functions so I'm trying to think of a better approach

[Vlad Tsyrklevich]

Daniel Weber said:

A potential way to automatically prove these implications is to use Vampire, and for a bunch of a functions add the assumption $\text{injective}(f) \leftrightarrow \text{surjective}(f)$, I can try to do that

I was trying to use Vampire for this, in an even simpler fashion, but I don't understand Vampire well enough and need time to read more

[Terence Tao]

Daniel Weber said:

Michael Bucko said:

Daniel Weber schrieb:

A potential way to automatically prove these implications is to use Vampire, and for a bunch of a functions add the assumption $\text{injective}(f) \leftrightarrow \text{surjective}(f)$, I can try to do that

Daniel, could you please somehow share those snippets / screenshots, or document how you're working with Vampire? That'd be very helpful.

I haven't done this yet, as there are many such functions so I'm trying to think of a better approach

I think just asserting injective <-> surjective for left multiplication, right multiplication, and squaring should already handle most applications that we know of. One could update this list manually as new challenging implications come in that require anything beyond this.

[Will Sawin]

If it becomes necessary, you could also take functions defined using all subexpressions on either side of the equation, like if the equation involves the expression x * (x * y) you could add these axioms for x * (x * y) viewed as a function of x for fixed y and viewed as a function of y for fixed x.

[Vlad Tsyrklevich]

The current status is I'm able to resolve about 40% of open finite implications, and I'll give Vampire a go next and use that 40% as a benchmark to verify against.

[Vlad Tsyrklevich]

Quick update: To get something working I started generating proofs simply using Vampire with additional laws of the form $x=f^{-1}(f(x))$ for any inverses I could find of $x=f(f^{-1}(x))$ as I already had a lot of this implemented from the previous scripts. This solves 200/320 open finite implications (and also works for the implications of the three order 5/6 Austin laws.) This is implemented and verified in Lean.

I've run some tests locally adding bi-implications for left/right mul and squaring and the numbers are better, but as it's quite likely that's buggy since I don't have the Lean proofs to verify, I won't report them just yet. I need to investigate how painful adding parsing/conversion for the resulting Vampire proofs will be. In case anyone wants to double check me or is curious, the TPTP I'm using for this local test is (note: ![...] is $\forall$ and ?[...] is $\exists$):

fof(left_mul_inj_surj, axiom, ![A,M] : ?[B] : A = mul(M, B) <=> ![X, Y, M] : (mul(M, X) = mul(M, Y) => X=Y) ).
fof(right_mul_inj_surj, axiom, ![A,M] : ?[B] : A = mul(B, M) <=> ![X, Y, M] : (mul(X, M) = mul(Y, M) => X=Y) ).
fof(square_inj_surj, axiom, ![A] : ?[B] : A = mul(B, B) <=> ![X, Y] : (mul(X, X) = mul(Y, Y) => X=Y) ).

[Vlad Tsyrklevich]

One more note on an equation I ran across: Equation 1133 is $x=y((y(zy))x)$, with $f(x)=yx$ and $f^{-1}(x)=(y(zy))x$ it could also be re-written $x=f^{-1}(f(x))=(y(zy))(yx)$. This is Equation 1979, which 1133 is equivalent to ({1133,1979} is the entire equivalence class.) I don't know if there's anything interesting about this phenomena, but I thought I would note it.

[Vlad Tsyrklevich]

The conversion is trickier than I expected, mostly because I'm just over my head trying to use @Daniel Weber's tooling. The conversion from Vampire to Lean with the new rules is not completely trivial as the introduction of implications/disjunctions complicates the conversion. Daniel was able to make it work in Greedy, but I'm not as skilled as him in Lean.

By chance looking around though I found Duper and using it locally for tests has been really simple, check out how trivial this is to prove a finite implication using the method above:

lemma left_mul_inj_surj (G: Type _) [Magma G] [Finite G] : (∀ X0 X1 : G, ∃ X2 : G, (X1 ◇ X2) = X0) -> (∀ X3 X4 X5 : G, ((X5 ◇ X3) = (X5 ◇ X4)) -> X3=X4) := by
  intro ha _ _ x _
  let f (s : G) := x ◇ s
  have surj : Function.Surjective f := by
    repeat intro
    simp [f, ha]
  have inj : Function.Injective f := by simp [Finite.injective_iff_surjective, surj]
  apply inj (by assumption)

example (G: Type _) [Magma G] [Finite G] (h: Equation1076 G) : Equation151 G := by
  duper [h, left_mul_inj_surj]

example (G: Type _) [Magma G] [Finite G] (h: Equation1110 G) : Equation8 G := by
  duper [h, left_mul_inj_surj]

I took a couple random implications off of the equation explorer and it could solve them as well. I tried 1689=>2 and I believe it worked but proof reconstruction failed (that's my interpretation of duper#30).

I will take a stab at this approach and see how well it compares to what we get with Vampire and what the build times are like. However, more generally, this is kind of a nice tool, at least for working with implications. It's too bad we hadn't found this earlier, as it may have been useful in the early days when having a Lean-native ATP would have made filling out the implication graph very easy (though again, I'm unsure about build times.)

[Josh Clune]

Vlad Tsyrklevich said:

I took a couple random implications off of the equation explorer and it could solve them as well. I tried 1689=>2 and I believe it worked but proof reconstruction failed (that's my interpretation of duper#30).

Thanks for making  duper#30, I'll work on figuring out what's going wrong there and push a fix as soon as I'm able. In the meantime, if you use set_option simultaneousSuperposition false, Duper should be able to solve 1689=>2 without a proof reconstruction error (long term, I don't intend for that to be an option you should have to set, but hopefully it can serve as a workaround while I debug duper#30).

[Vlad Tsyrklevich]

So duper is able to solve many implications, but there also quite a few it times out on. I am able to coax it into finding them by giving it intermediate steps from Vampire, but now that I'm able to verify that this approach works, and check steps I'm not confident in, I've put down the Vampire->Lean conversion for now and gotten back to researching the fundamental approach.

I went back to looking at how 'complete' the results for left mul/right mul/inverses are, and there's a lot more we can gain than those alone. By bruteforcing additional axioms I was able to come up with a more complete set, but this approach is unideal as I'm only checking a single axiom at a time, and it's possible that some refutation requires a combination. I can't simply give every single possible rule to vampire as it fairly quickly is unable to solve implications it was previously able to.

There are a couple of approaches here: bruteforcing individual axioms and building up the minimal set we needed for previous implications and then trying on top of those, trying to use the implication graph somehow, inverses could still be useful. Perhaps finiteness gives us some other property that could be useful to give Vampire here? This is an interesting example where finding finite implications is slightly more difficult than finding them generally, as the number of additional axioms we give the ATP begins to overwhelm it.

[Vlad Tsyrklevich]

Another idea is to try using a higher-order ATP and feed it the general injectivity <=> surjectivity rule, though I suspect the state space explosion would render the approach useless.

[Vlad Tsyrklevich]

Also I'm not bruteforcing with the complete list of possible bijectivity rules right now, in the case the LHS is $x ◇ y$ I am overly conservative in which rules I produce. This is related to what Will Sawin mentioned earlier with keeping individual variables constant. I need to go through and improve the choices I make there and ensure I'm doing so correctly. I'm also only currently generating bijectivity rules up to order 4 right now, and perhaps to solve some implication we actually need to go to higher orders?

[Vlad Tsyrklevich]

Anyways, there are 311 open finite implications on main, I have formalized solutions to 200, and another 85 I believe should be correct, leaving only 26 left, so perhaps instead of finding the correct solution I should just look at the individual cases instead. The list is:

List

1076,2294
1076,4435
1110,1629
1112,1629
1486,3862
1486,3877
1516,1489
1518,3862
1518,47
1518,614
1518,817
1728,99
3308,3456
3308,3511
3342,3456
3342,3522
3342,4065
3342,4118
3549,3862
3549,3955
854,1045
854,1055
854,3316
854,3925
854,413
879,4065

[Matthew Bolan]

If you find a finite counterexample to 1486 -> 3877, it can be promoted via the twisting method to a finite counterexample to 1486 -> 3862. Given a magma $(M,\diamond)$ satisfying 1486 and not 3877 , we can define a new 1486 magma $(M\times M, *)$ by $(x_1,y_1)*(x_2,y_2) = (y_1\diamond y_2, x_1 \diamond x_2)$, and if I've done my algebra correctly this new magma will be a counterexample to 1486 -> 3862. There is no way around the need for a 3877 counterexample, the twisting monoid for 1486 is $\langle T, U | T^2=1;T=U\rangle$, while for 3877 it is $\langle T, U | T^3=T;T=U\rangle$, so we can't twist something satisfying both 1486 and 3877 and get something satisfying 1486 but not 3877.

[Matthew Bolan]

(This is the only implication on your list where twisting does anything)

[Vlad Tsyrklevich]

Currently, I believe I have (non-formalized) finite implications for everything but the 4 from 3308/3549.

[Matthew Bolan]

Oh, awesome!

[Terence Tao]

Huh, you may complete the finite implication graph before the original implication graph is complete!

[Vlad Tsyrklevich]

Well, implications are a lot easier, and filling out the finite graph has mostly been finding implications.

[Matthew Bolan]

So do you believe the remaining 4 implications are true or false?

[Vlad Tsyrklevich]

I'm not sure. The brute force approach I took may be incomplete, and I haven't finished figuring out if I could use more values. Let me explain. I was able to solve the remaining implications by using a pretty basic brute force algorithm, where I picked an LHS, call it $f(x)$, and then tried different inputs, e.g. $f(x◇y)$, $f(x◇(y◇x))$, etc. and used those as values to $surjective ↔ injective$. However, this will never generate equations like 3308 ($x ◇ y = x ◇ (x ◇ (y ◇ x))$) or 3549 ($x ◇ y = y ◇ ((x ◇ y) ◇ y)$) because the RHS is not of the form $f(LHS)$.

I tried to think about what statements I could make about such equations, and I never came to a conclusion. For example, for equation 343 ($x ◇ y = z ◇ (x ◇ y)$) I can say that holding x and y constant, that surjectivity implies injectivity:
fof(eq343_bij_y, axiom, ![X,Y,Z] : ?[T] : ( mul(X, Y) = mul(Z, mul(X, T)) ) <=> ![T1,T2,Z,X] : ( (mul(Z, mul(X, T1)) = mul(Z, mul(X, T2)) ) => mul(X, T1) = mul(X, T2) )). fof(eq343_bij_x, axiom, ![X,Y,Z] : ?[T] : ( mul(X, Y) = mul(Z, mul(T, Y)) ) <=> ![T1,T2,Z,Y] : ( (mul(Z, mul(T1, Y)) = mul(Z, mul(T2, Y)) ) => mul(T1, Y) = mul(T2, Y) )).

EDIT: This bijection is incorrect

Can I make any such statements about eq323, $x ◇ y = x ◇ (x ◇ y)$?

[Terence Tao]

The remaining implications follow from

Lemma 1: Let $X$ be finite, and let $f, g: X \to X$ be such that $f = f \circ f \circ g$. Then $f = f \circ g \circ f$.

Proof: Call a point $x \in X$ periodic if $f^n(x) = x$ for some $n>0$. Because the forward orbit $x, f(x), f^2(x), \dots$ in a finite space $X$ must repeat, we see that for each $x$ there exists an $n$ such that $f^n(x)$ is periodic. Let $n_x$ be the first $n$ for which this occurs. If $n_x > 1$, then $g(x), f(g(x)), f(f(g(x))$ cannot be periodic (as this would imply $f(x)$ periodic), and then we can see that $n_{g(x)} = n_x + 1$. Hence the maximal value of $n_x$ is at most $1$, which implies that $f(x)$ is periodic for every $x$. Thus there is an $n > 1$ such that $f^n = f$. Since $f = f^2 \circ g$, we have $f^n = f^{n-2} \circ f \circ f = f^{n-2} \circ (f^2 \circ g) \circ f = f^n \circ g \circ f = f \circ g \circ f$, as desired.

3308 states that $f = L_x, g = R_x$ obeys the hypotheses of Lemma 1, which gives the desired implications. For 3549, one can similarly argue by applying $f = R_y, g = L_y$ to the following variant lemma:

Lemma 2: Let $X$ be finite, and let $f, g: X \to X$ be such that $f = g \circ f \circ f$. Then $f = f \circ g \circ f$.

Proof: By hypothesis, $f^2(x)$ uniquely determines $f(x)$. This prevents $n_x = 2$ for any $x$ (because if $n>2$ is such that $f^{n+2}(x) = f^2(x)$, then $f^{n+1}(x) \neq f(x)$), and hence also prevents $n_x > 2$ for any $x$. So again we have $f(x)$ periodic for all $x$, so $f^n = f$ for some $n>1$. Then $f = f^n = f \circ (g \circ f^2) \circ f^{n-2} = f \circ g \circ f^n = f \circ g \circ f$ as required.

[Vlad Tsyrklevich]

Cool! This is a powerful method, I wonder if it's stronger than surjective↔injective

[Vlad Tsyrklevich]

Both of these lemmas are directly related to the original method I was using of finding inverses, in that case I used that $x=f(g(x)) → x=g(f(x))$, and the final statement of the lemmas above are derivable from the original assumption by applying $f$. It's funny, I had assumed that the original method didn't have enough generality to cover more cases, but clearly I was not looking hard enough.

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

I wonder if it's stronger than surjective↔injective

Having given this idea a little more thought, I'm not sure that it offers any new axioms for equations with LHS of just 'x' so how could it be stronger.

[Alex Meiburg]

Just curious, so you have the finite implications complete, do you have witnesses to all of the finite non-implications? That would be surprisingly fast because I was of the impression that some of the non-implications were proved with infinite magmas, even though it didn't necessarily seem that there would be an implication in the finite case.

If you don't, how do you know which will be implications or non-implications?

[Alex Meiburg]

(I'm probably misunderstanding one thing or another)

[Vlad Tsyrklevich]

The original answer was "All remaining finite unknowns were implications", but writing this it actually seemed somewhat far-fetched, so I began to double check and I'm sorry to report that at least some of the implications I had conjecturally resolved relied on a faulty premise. I will need some time to go through and verify everything to understand how many finite unknowns remain open.

[Vlad Tsyrklevich]

Current status: equational#797 has the implications that I've already formalized in Lean, and I will shortly propose another change (equational#804) to add a number of finite conjectures: first the ones Terence solved above, and second, the injective<->bijective ones I have been able to verify using Duper. I don't think Duper is suitable to upstream due to versioning issues, but it should eliminate any risk that I've made any more mistakes. There was only one injective<->bijective implication I believe is correct that I did not succeed in making Duper recognize, 1516->255. I upload the Duper verified conjectures here so I can link them from Conjectures.lean. DuperConjectures1.lean

[Vlad Tsyrklevich]

The remaining balance is 30 unknowns modulo duality, equivalence class, and conjectures. I will take a look at how feasible it is to add a finite graph view to the equation explorer and graphiti next.

[Matthew Bolan]

Is the list of unknown finite implications somewhere?

[Vlad Tsyrklevich]

List after equational#797 and equational#804

1076,2294
1076,4435
1110,1629
1112,1629
1486,3862
1486,3877
1516,1489
1516,255**
1518,3862
1518,47
1518,614
1518,817
1728,99
3342,3456
3342,3522
3342,4065
3342,4118
476,359
476,4065
503,359
503,3862
503,4065
677,255
854,1045
854,1055
854,3316
854,3925
854,413
879,4065
906,3862

[Matthew Bolan]

Where did the table here come from https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/Refutation924.lean#L20 ?

[Alex Meiburg]

Those are all generated (hence) the name by another program, in this case from https://github.com/teorth/equational_theories/tree/main/equational_theories/Generated/All4x4Tables/src

[Matthew Bolan]

I gathered that, but which other program? This particular table didn't look to me as if it could have come from any of those programs, but I gave it only a cursory glance.

[Vlad Tsyrklevich]

By searching for that table in https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/data/plan.txt, you can find it on line 3698, using blame on the top left in github, you can find that it was recently added by Daniel, importing vampire refutations to the All4x4Tables

[Matthew Bolan]

There are other tables in this folder which clearly came from ATP, for example I think I recognize the strange 12x12 854 magma and the 32x32 1485 magma.

[Vlad Tsyrklevich]

Agh, that's the plan though, not where it came from. Anyways it's also from vampire-generated.txt but that explanation was the wrong way to find that info

[Matthew Bolan]

Thank you, I missed that file somehow.

[Terence Tao]

opened equational#809 to formalize the two lemmas about functions on finite sets used above to prove implications on finite magmas.

[Matthew Bolan]

Matthew Bolan said:

Where did the table here come from https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/Refutation924.lean#L20 ?

This table remains very impressive to me. Even imitating the vampire script which I assume found it (and allocating vampire more time), I am unable to coax vampire into outputting it. What did you do to find this thing @Daniel Weber ?

[Vlad Tsyrklevich]

Don't know if you've seen this already, but I presume it's from equational_theories/Generated/VampireProven/src/vampire_fin_counterexamples.py which has the vampire command in there

[Matthew Bolan]

I can't quite coax that into giving me this table either. I'm guessing some small modification to the schedule there will get it though.

[Daniel Weber]

Searching the git history, it was generated as a counterexample to 1486 -> 2052 with vampire_fin_counterexamples.py

[Matthew Bolan]

Ah, that explains a lot. I tried generating it from the things it is currently listed as a counterexample to, (for some I even found smaller tables, like this one), but 2052 is not currently among them.

[Terence Tao]

For some of the outstanding implications on the finite magma graph, one could try filling in a translation invariant model of some fixed size, e.g., 10, using an ATP (possibly inserting explicitly the assertion that squaring is a bijection for such models, in case it speeds things up).

[Terence Tao]

Here is a (positive) resolution of the four outstanding implications for 3342. Setting $Sx := x \diamond x$, $f x := x \diamond Sx$ and $Cx = Sx \diamond x$, the law is $x \diamond y= y \diamond fx$, and we will claim that $x \diamond y = Cx \diamond y$ and $x \diamond y = x \diamond Cy$ for finite magmas, giving the four open implications.

Note that $x \diamond y= y \diamond fx = fx \diamond fy$, hence $f$ is a homomorphism.

On a finite magma, we have some eventual period $n \geq 1$ so that $f^n = f^{2n}$. From the law we have $Sx = S fx$, and $Cx = Sx \diamond x = f^n Sx \diamond f^n x = f^n Sx \diamond f^{2n} x = f^{2n-1} x \diamond f^n Sx = f^{n-1} x \diamond S x = f(f^{n-1} x) = f^n x$. Then

$Cx \diamond y = f^n x \diamond y = f^{2n} x \diamond f^n y = f^n x \diamond f^n y = x \diamond y$

and a similar argument gives $x \diamond Cy = x \diamond y$.

[Matthew Bolan]

I think the definition of $Cx$ should read $Cx = Sx \diamond x.$

[Terence Tao]

The implication 1516->255 for finite magmas was already established (because $L_{x^2}$ is surjective, hence bijective, hence $x = L_{x^2}^{-3} x^2$, so squaring is invertible, and 255 is known for squares); see the summary at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/1516.20-.3E.20255/near/478524073

[Ibrahim Tencer]

That should say 3342 instead of 3844 right?

[Vlad Tsyrklevich]

Terence Tao said:

Here is a (positive) resolution of the four outstanding implications for 3342

I have this formalized, there's still some clean-up I need to do but figured I'd mention it here in order to avoid duplicating work with anyone else.

[Terence Tao]

I wrote up the proof of these implications in the blueprint at equational#844 so if you want to formalize them you can also add \leanok's to the blueprint.

[Terence Tao]

Attached at counterexample.txt
is a finite (order 84) counterexample to 503 -> 4065, 3862, refuting a net of 6 implications for finite magmas. (It also contains a link to Finite Magma Explorer, but the link is too large to put directly into Zulip.) Incidentally one should update FME to check against the finite implication table rather than the infinite implication table, as currently it does not register this as a new refutation. [EDIT: opened equational#855 for this.]

Some words on how I constructed this example. Equation 503 reads $L_y^2 (x \diamond L_y x) = x$. In finite magmas, the $L_y$ are all invertible permutations, so this is equivalent to $x \diamond L_y x = L_y^{-2} x$, which in turn is equivalent to $L_y^2 x \diamond L_y^3 x = x$. I interpret this as follows: if the permutation $L_y$ contains a cycle $[x_1,x_2,\dots,x_n]$, then we must have $x_{i+2} \diamond x_{i+3} = x_{i}$ for all $i$ (where we extend $x_i$ periodically by $n$). In particular each $L_{x_{i+2}}$ then must have a cycle that contains a portion $[\dots, x_{i+3}, x_i, \dots]$. One nice thing about this law is that the conclusion does not actually involve $y$ directly, but only the cycles generated by $L_y$.

So it becomes a question of seeing how cycles propagate to create other cycles, without causing collisions. From the rule we see that it becomes advantageous to reuse cycles as much as possible: if there was already a cycle that was of the form $[\dots, x_{i+3}, x_i, \dots]$ that does not intersect with any previously defined values of $L_{x_{i+2}}$, then the cycle $[x_1,x_2,\dots,x_n]$ does not generate any new cycles to worry about at the $i$ index at least, if we simply add the old cycle to the definition of $L_{x_{i+2}}$.

Note that the right absorption law $x \diamond y = y$ obeys 503, which corresponds to all cycles being of length $1$. Now this of course will not produce counterexamples, but it does hint that we should try to stay close to this law (cf. the "modified base magma strategy"), and this leads to the idea that the permutations $L_y$ should be close to the identity map in that most cycles are just 1-cycles. In order for $L_y$ to have a 1-cycle $[x]$ it is necessary that $x$ be idempotent. If every element is idempotent then we do not have any counterexamples, so I deliberately looked for models with exactly one non-idempotent at 0, and all other elements idempotent. Now it is perfectly safe for each shift $L_y$ to have a 1-cycle $[x]$ as long as $x \neq 0$. As a consequence, it now becomes perfectly safe for each shift $L_y$ to have a $3$-cycle $[x_1,x_2,x_3]$ with $x_1,x_2,x_3 \neq 0$, as this only generates safe singleton cycles.

So now I tried a greedy algorithm that I plan to terminate in finite time, iterating the cycle generation procedure until I am just left with fragments that I can close up and complete using 3-cycles and 1-cycles. All the fragments $[\dots, x_{i+3}, x_i, \dots]$ generated by the above cycle propagation rule for a given shift $L_y$ are going to be fine (if the magma is large enough) because we can close them up into a 3-cycle that involves an element that hasn't been used previously - unless they are adjacent to another fragment, in which case they need to be closed up into some longer cycle; I ended up mostly using 10-cycles when this occurred, because at that size the further cycle fragments that were generated no longer cause problems.

It took a lot of trial and error (and python code, which I attach if anyone is interested at
magma.py)
, but I was able to start with the cycle $[0,1,2,3]$ for $L_0$ (which is already enough to contradict all the outstanding implications, if it can be completed to full magma) and iterated, using new elements whenever needed to avoid cancellations. For instance, in my construction $L_1$ contained the cycle $[26, 4,   5, 0, 6,  2,  3,   7,  8,  9]$, $L_2$ contained the cycle $[1,   10,  3, 0, 11, 12, 28, 13, 14, 15]$, and $L_3$ contained the cycle $[26, 2,  16, 0, 1,  17, 28, 18, 19, 20]$. This mostly generates disconnected fragments that are easy to close up, but there are a couple bad cases remaining (primarily involving fragments that contain the non-idempotent 0) that required quite a bit of ad hoc fiddling to dispose of, but in the end I was able to close all the cycles and get the magma in the file above.

It may be possible to compress this example into a smaller form, perhaps using ATP assistance; I don't know if this order 84 example is too large for Lean to handle.

[Terence Tao]

For what it's worth, equation 476, which had been previously flagged as a "mysterious twin" to 503, has a similar interpretation $L_y x \diamond L_y^3 x = x$, so the only difference is that the cycle fragment $[\dots, x_{i+3}, x_i, \dots]$ is assigned to $L_{x_{i+1}}$ rather than $L_{x_{i+2}}$. So presumably a similar technique will handle the two implications coming out of 476; I might try this later if I have some free time. EDIT: actually, the two laws may be "definably equivalent" in the finite case at least, so that there is some way to transform the existing magma to refute the 476 implications also. Will look into this now.

[Douglas McNeil]

Wow, I thought the days of the finite magma contributions were over! I think you can get down to order 77 but still satisfy 503 and violate 4065, 3862 just by removing single elements which preserve the demonstration, but that's only a modest improvement.

[Terence Tao]

I finally have an explanation for the "twinning" of 476 and 503. If $\diamond$ solves 503, with all the $L_y$ invertible, then we can create a 476 operation $\tilde \diamond$ by requiring that the left multiplication $\tilde L_y$ operation for $\tilde \diamond$ is the inverse of the left multiplication for $L_y$:

$y \diamond x = z \iff y \tilde \diamond z = x.$

It is then a routine matter to verify that $\tilde \diamond$ obeys 476 if and only if $\diamond$ obeys 503.

Applying this to the previous example, I now have a finite magma (also of order 84) that refutes 476 -> 359, 4065:
counterexample-dual.txt
Weirdly, the twinning is not perfect: for finite magmas, 476 implies 3862, but 503 does not.

[Vlad Tsyrklevich]

Douglas McNeil said:

Wow, I thought the days of the finite magma contributions were over!

I think the finite unknowns likely have both implications and refutations still remaining. I think some may not even be that difficult, but the infinite refutation was just easier than the finite one.

[Vlad Tsyrklevich]

Terence Tao said:

I don't know if this order 84 example is too large for Lean to handle.

I think this should be doable, 503 and 476 are two variable equations so this should only be ~$84^2$ operations to check which is still very small. The destination equations are one variable so it's probably not even worth optimizing it by finding a specific counterexample for Lean to check.

Incidentally, @Douglas McNeil $77^2/84^2$ is still a ~15% improvement so if you have the magma still handy I can try to feed it to Lean and see how it responds.

EDIT: Turns out I was wrong, Lean hits a deterministic timeout, even if I quadruple the maxHeartbeats.

[Douglas McNeil]

red77.txt

^ here it is, FWIW.

[Vlad Tsyrklevich]

Even this requires ~90s and maxHeartbeats 1.75 million to finish, that seems somewhat out-of-proportion to the computational difficulty of this check, but I have no idea what's going on inside of Lean.

[Bernhard Reinke]

Here is a variant of injective <-> surjective that might be useful: If $S$ is a finite set and $f \colon S \rightarrow P(S)$ a map
such that $f(s)$ is nonempty for all $s \in S$ and $f(s) \cap f(t) = \empty$ for all $s \not= t$, then $f(s) = \{g(s)\}$ for some bijection $g \colon S \rightarrow S$. This should be easily provable by counting, first establishing that $f(s)$ has to be a singleton, then that $g$ is defined and injective, hence a bijection.

This can be useful to formalize 1701 => 4587 (it seems this was already proven by duper?): here we can take $f(x) = \{ (y \diamond x) \diamond x | y \in S\}$. 4587 is equivalent to $f(x)$ being a singleton for all $x$, and we get by the functional equation that they have to be disjoint (as $y \diamond z = x$ for $y,z \in f(x)$).

[Vlad Tsyrklevich]

Bernhard Reinke said:

it seems this was already proven by duper?

Everything duper-verified was found using injective<->surjective, but the duper proofs aren't upstream-able.

[Terence Tao]

I've marked the 503 and 476 refutations as conjectures for now.

It may be possible to compress the example further by identifying elements. For any given element $x$, the sets $F_x := \{ y: y \diamond x \neq x \}$ are quite small typically in this example. If there are $x,x'$ with $F_x, F_{x'}$ disjoint and with the property that for any $y$, $x \diamond y, x' \diamond y, y$ are not all distinct, one can try to combine them into a single element $x''$ by setting $x'' \diamond y$ equal to the choice of $x \diamond y$, $x' \diamond y$ not equal to $y$ if such a choice exists, or $y$ otherwise, and also setting $y \diamond x''$ equal to $y \diamond x$ for $y \in F_x$, $y \diamond x'$ for $y \in F_{x'}$, and $x''$ otherwise. It's not completely guaranteed that this will produce a new counterexample, but for the rows and columns where $E_x, F_x$ are very small, this should happen fairly often, so one could iteratively search for valid compressions by computer perhaps.

Also, I think one can formalize in Lean the way to convert a 503 counterexample to a 476 counterexample, so one only has to do the big verification for one counterexample rather than two.

[Douglas McNeil]

Down to order 50, following that technique:

red50.txt

[Vlad Tsyrklevich]

We get a better-than-I-would-expect reduction here ($77^2/50^2 \approx 2.3$), this builds in 13s, requires a maxHeartbeats of ~300k

[Vlad Tsyrklevich]

If we can get it down to 45 I think it would build without requiring maxHeartbeats changes

[Terence Tao]

The law 503 is automatically true when $y \diamond x = x$ and $x$ is idempotent. This should cover a large fraction of the cases, as by design every element except $0$ is idempotent. It may be possible to then do a custom verification of 503 that is slightly faster than the brute force computation.

[Vlad Tsyrklevich]

I built a simple heuristic bruteforcer to find other proofs by periodicity as Terence did with 3342 above. I simply took all single-variable functions up to order 3, and then searched for implications with the additional axiom $f^i = f^{i*j}$ with a number of different values for i and j. For 3342, with the function that Terence used, $f=x \diamond (x \diamond x)$, vampire found the implication with all values of i,j that I tested with, but for all other tested functions it found at most 1 positive hit. Even for expressions like $f^1 = f^8$ that took ~50kb to represent as an axiom in TPTP, vampire still completed the proof in <0.1s

This is useful for finding other possible implications of this style, but obviously is incomplete and doesn't establish full evidence for the existence of such a proof. It would also be closer to the style of the original proof to try only with functions that are a shared sub-expression of the two ends of the implication, but I wanted to go fishing for other possibly interesting behavior we might find so I searched all functions up to order 3.

Looking specifically for functions that had implications for all tested values of (i,j), it found multiple hits in the current list of conjectures, but no hits among the unknowns. So this may still be useful for formalizing those unknowns, if converting the bijections proofs with vampire proves too painful, but found nothing new.

[Vlad Tsyrklevich]

Crazy, there are still finite refutations left that are captured by just an 8x8 magma https://teorth.github.io/equational_theories/fme/?magma=%5B%5B1%2C0%2C3%2C2%2C4%2C5%2C6%2C7%5D%2C%5B2%2C5%2C3%2C4%2C0%2C1%2C6%2C7%5D%2C%5B4%2C1%2C3%2C2%2C0%2C5%2C6%2C7%5D%2C%5B1%2C0%2C3%2C2%2C7%2C5%2C6%2C4%5D%2C%5B6%2C1%2C3%2C2%2C4%2C5%2C0%2C7%5D%2C%5B4%2C5%2C0%2C2%2C3%2C1%2C6%2C7%5D%2C%5B0%2C1%2C3%2C2%2C4%2C5%2C6%2C7%5D%2C%5B1%2C0%2C3%2C2%2C4%2C5%2C6%2C7%5D%5D

[Vlad Tsyrklevich]

To be fair, I guess order is perhaps a poor measure of complexity, since equations that are towards the top of the Hasse diagram will allow many models so it takes longer to search through a given order compared to others that don't. But this is just by simple exhaustive search, though I have now optimized the mace4 parameters I use for every given implication after learning about them from @Jose Brox

[Vlad Tsyrklevich]

I timed the amount of time it took to search through a given order with different parameters and I was surprised by how large a difference it can make.

[Vlad Tsyrklevich]

Another negative result: I had been meaning to try this for a while, currently I've checked for finite implications by looking at the inverses of the source and target of a given unknown implication, but what about inverses of other implications of the source? I wired up a script that consumes the output of an ATP printing equivalent laws, and fed inverses of any equivalent laws back into the TPTP on repeat. The method is kind of interesting because it's trying to move through the infinite graph of implications by essentially making a hacky duct-taped "finite ATP", but it didn't find anything new in order 4 or 5.

[Terence Tao]

Some cute observations about finite 1518 models (but no new implications, unfortunately).

The equation reads $x = L_{Sy} L_x L_y x$, so $L_{Sy}$ is surjective, hence bijective on finite magmas. 1518 implies 359, $Sx = L_{Sx} x$, hence $x = L_{Sx}^{-1} Sx$; so squaring is injective, hence bijective. So in fact all the $L_y$ are bijective, so finite 1518 magmas are left-cancellative.

This gives the following weird symmetry: define a new operation $\tilde \diamond$ by $x \tilde \diamond y = L_x^{-1} y$, so $\tilde L_x = L_x^{-1}$. Then $x = L_{Sx}^{-1} Sx$ becomes $x = \tilde S S x$; squaring in this new magma inverts squaring in the old magma. Also, rewriting 1518 as $L_{y}^{-1} L_x^{-1} L_{Sy}^{-1} x = x$ and setting $\tilde y= Sy$ we obtain $\tilde L_{\tilde S \tilde y} \tilde L_x \tilde L_{\tilde y} x = x$, so this reflected magma also obeys 1518.

I checked that the outstanding implications 47, 617, 817, 3862 are unchanged under this symmetry (and thanks to 359, the claims 617 and 47 are in fact equivalent). Not sure where to take this further though.

[Douglas McNeil]

@Vlad Tsyrklevich : I had a thought yesterday. To complete the finite side, does that mean someone's going to have to get 854=/>413 or prove there's no finite counterexample? :scared:

[Terence Tao]

Yeah, a large fraction of the remaining unresolved finite implications are coming from familiar nemeses like 854 where we were barely able to get a resolution in the infinite case by either greedy methods or confluence methods. There seem to be some genuinely difficult problems in there!

I played a bit with 1110=>1629 since it had the appealing form $L_y R_y L_y S = I \implies Sx \diamond Cx = x$ (where as usual $Sx = x \diamond x$ and $Cx = Sx \diamond x$). Immediately one gets that $L_y, R_y, S$ are bijections so that one can permute to get $R_y L_y S L_y = I$, $L_y S L_y R_y = I$, and $S L_y R_y L_y = I$. This gives some cute identities:

Lemma 1: $x \diamond Sx = x$ (equation 8)

Proof: Set $y = x \diamond S x = L_x R_x x$, then $L_x L_y x = L_x R_x L_x S x = x$. Also $L_x L_y y = L_x S L_x R_x x = x$. Cancelling, we obtain $x=y$ as required. $\Box$

Lemma 2: $SCx = CSx$.

Proof: On the one hand we have $S(x \diamond Cx) = S L_x R_x L_x x = x$, so $S(Sx \diamond CSx) = Sx$ and hence $Sx \diamond CSx = x$. On the other hand $Sx \diamond SCx = L_{Sx} S L_{Sx} x = L_{Sx} S L_{Sx} R_{Sx} x = x$. Cancelling, we obtain $CSx = SCx$ as required. $\Box$

The latter is hinting at an abelian translation invariant model (which would automatically have commuting squaring and commuting maps) but I checked by brute force computer calculation that no model on any cyclic group of order up to 12 is available. (I should try other abelian groups like $F_2^n$ though.)

EDIT: Since $Sx \diamond CSx = x$, equation 1629 is equivalent to $CSx = Cx$, so in translation invariant models (in which cubing is a bijection) it collapses to the idempotent law $Sx=x$; in general 1629 is equivalent to the claim that cubes are idempotent. The only translation invariant model I currently know of is the linear model $x \diamond y = x + a(y-x)$ on a ring $M$ where the coefficient $a$ obeys the equation $a(1-a)^2 = 1$, but such models are unfortunately idempotent. In fact it seems that all linear models (commutative or otherwise) obey 1629. One such model is $x \diamond y = \phi x - y$ where $\phi$ obeys the golden ratio equation $\phi^2 = \phi+1$; now we don't have idempotency, but instead the cubing map is identically zero, which forces $CSx = Cx$ for a different reason.

[Matthew Bolan]

1486 isn't quite 1485, but it is still implied by 168 and so much of the directed graph machinery carries over. 1486 also has anti-implications falsified by some impressively large finite models (for example a 21x21 table!) found by vampire. As I observed above it also admits non-trivial twists, which has the consequence that it suffices to give a table refuting 1486 -> 3877.

[Matthew Bolan]

I also notice that there are still some open implications from 1076 and 879, which have not yet been formalized even in the infinite case. I've tried to search for finite models of these through various means with no luck.

[Vlad Tsyrklevich]

Douglas McNeil said:

someone's going to have to get 854=/>413 or prove there's no finite counterexample

Indeed, and one interesting thing I think about the finite graph is that unlike with the general graph, it's not clear to me which of the remaining unknowns may be implications, though others with a greater degree of mathematical sophistication may be able to derive educated opinions on the matter.

[Matthew Bolan]

To record the graph version of 1486 x = (y ◇ x) ◇ (x ◇ (z ◇ z)):
We ask for a directed graph with a notion of "good" paths of length 2 satisfying:
Claim 1 Any two points are connected by exactly one good path.
Claim 2 Any directed edge is the first edge of some good path.
Claim 3 if $a \to b \to c$, $c \to d \to e$, $f \to e \to f$ are good, then $b \to c \to d$ is good.

Given such a directed graph, we can place the structure of a 1486 magma on its vertices by defining $x \diamond y$ to be the midpoint $z$ of the unique good path $x \to z \to y$. Claim 3 is so that 1486 is satisfied. Conversely, given a 1486 magma, letting $x \to y$ mean that $y = x \diamond z$ for some $z$, we have that $y \to y \diamond x$ trivially, and $y \diamond x \to x$ by 1486, so we can take our notion of good path to be a path of the form $x \to x \diamond y \to y$. Claim 1 obviously holds, Claim 2 holds as if $x \to y$ then there exists $z$ with $y=x \diamond z$, and then $x \to y \to z$ is good. Finally, 1486 implies Claim 3 for this graph.

Unlike 1485, we know a model of 1486 which is not of size $n^2$ or $2n^2$, this order 21 example which falsified most of its outstanding implications.

[Matthew Bolan]

It seems the smallest 1486 magma which is not of size $n^2$ or $2n^2$ is order 11, for example this one. I also found this degree 13 example. Actually, for $2 n^2$, I only have an example of order 18

[Vlad Tsyrklevich]

Daniel Weber said:

Searching the git history, it was generated as a counterexample to 1486 -> 2052 with vampire_fin_counterexamples.py

How did you generate your finsched.sch? My build of vampire doesn't seem to like it, and I don't see any of the lines in the git history of Vampire's CASC/Schedules.cpp and couldn't find much info about schedules online.

[Matthew Bolan]

I think it is a modified version of the schedule for casc_sat, but I only glanced at it briefly.

[Vlad Tsyrklevich]

Ah, indeed. Now I do see some of these lines in CASC/Schedules.cpp, vim was interpreting the + as a regexp instead of a char while I was searching.

[Vlad Tsyrklevich]

Using the Linux version downloaded from their website instead of my locally-built macOS one also resolves the remaining issues I had.

[Daniel Weber]

Matthew Bolan said:

I think it is a modified version of the schedule for casc_sat, but I only glanced at it briefly.

Indeed, it's simply just the fmb parts from the casc_sat schedule

[Vlad Tsyrklevich]

1728 =/> 99. That was easy, just using vampire.

[Matthew Bolan]

Ack, I messed up here. Claim 3 does not hold for all graphs produced this way, in fact my order 11 one gives rise to a counterexample.
Matthew Bolan said:

To record the graph version of 1486 x = (y ◇ x) ◇ (x ◇ (z ◇ z)):
We ask for a directed graph with a notion of "good" paths of length 2 satisfying:
Claim 1 Any two points are connected by exactly one good path.
Claim 2 Any directed edge is the first edge of some good path.
Claim 3 Any directed edge is the last edge of some good path.
Claim 4 if $a \to b \to c$, $c \to d \to e$, $f \to e \to f$ are good, then $b \to c \to d$ is good.

Given such a directed graph, we can place the structure of a 1486 magma on its vertices by defining $x \diamond y$ to be the midpoint $z$ of the unique good path $x \to z \to y$. Claim 4 is so that 1486 is satisfied. Conversely, given a 1486 magma, letting $x \to y$ mean that $y = x \diamond z$ for some $z$, we have that $y \to y \diamond x$ trivially, and $y \diamond x \to x$ by 1486, so we can take our notion of good path to be a path of the form $x \to x \diamond y \to y$. 1486 implies Claim 4 for this graph.

Unlike 1485, we know a model of 1486 which is not of size $n^2$ or $2n^2$, this order 21 example which falsified most of its outstanding implications.

[Matthew Bolan]

I think I can just drop claim 3 and then everything will work out. I only needed claims 2 and 3 to prevent any spurious edges in the graph, but claim 2 already guarantees that the edge $x \to y$ in the graph becomes $y = x \diamond z$ in the magma.

[Terence Tao]

Small remark: the dual 2126 to 1486 has previously been discussed; it has a complete rewriting system, which is why we could resolve things in the infinite case, but not the finite case.

Just for the record, here is the current state of play with the finite graph (after 1728 is resolved) with the outstanding equations (and their duals), their implications (counting duality, which multiplies by a factor of 2) and how they were resolved for the infinite graph:

• 677 (dual 2910). 2 implications, previously established by the greedy method.
• 854 (dual 2712). 10 implications, previously established by a complicated greedy method or the unique factorization method.
• 879 (dual 2650). 2 implications, established by a (not yet formalized) greedy method.
• 906 (dual 2647), 2 implications, previously established by the greedy method.
• 1076 (dual 2531), 4 implications, established by a (not yet formalized) greedy method.
• 1110 (dual 2497), 2 implications, previously established by the confluent method.
• 1486 (dual 2126), 4 implications, previously established by the complete rewriting method.
• 1516 (dual 2091), 2 implications, previously established by a greedy method.
• 1518 (dual 2054), 8 implications, previously established by the greedy method.

[Matthew Bolan]

Woah 1516 has outstanding finite implications? Those would be really nice to find a finite counterexample to...

[Matthew Bolan]

No, you already refuted the finite implication 1516 -> 255.

[Matthew Bolan]

here https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/482527297

[Vlad Tsyrklevich]

1516 -> 1489 is still open.

[Matthew Bolan]

Ah, my bad. But that one has been formalized in the infinite case.

[Terence Tao]

You're right, I've adjusted the text accordingly.

[Matthew Bolan]

I notice that Vampire has this flag --fmb_detect_sort_bounds which has the description: "Use a saturation loop to detect sort bounds introduced by (for example) injective functions". Sounds useful!

I also noticed that the various sporadic magmas for law 1486 seem related, for example I can get a large portion of the table to agree between the 11x11 and 13x13 examples by doing some relabeling, and the 21 by 21 table contains many rows and columns which look like the ones coming from the smaller examples. I should get back to my "day job" though, so no more time to explore this tonight.

[Vlad Tsyrklevich]

Terence Tao said:

and how they were resolved for the infinite graph

I did not follow along closely enough to have a good understanding of it, but is confluence actually applicable in a finite context? Or any of the other general implication refutations for that matter.

[Terence Tao]

The way I understand it, confluence provides a way to determine whether two words $w,w'$ are equal in the free magma for a law, namely if their unique reductions agree. If their reductions do not agree, then this free magma then provides a counterexample to the implication that the law implies $w = w'$. But the free magma can be infinite, so this does not necessarily give a finite example. If we knew that the free magma had enough finite quotient that one could separate points, then we could also get a finite counterexample, but this doesn't have to be the case (in group theory, a classic example of this is the Higman group). That said, I don't know of a confluent law whose free magma didn't have enough finite quotients to separate points.

[Terence Tao]

A negative result: I checked the linear models for 1110 and 906 (hoping that we had simply overlooked this possibility in previous sweeps), but it looks like these implications are immune to both commutative and noncommutative models. 906 has a twisted idempotent model $x \diamond y = \omega y$ where $\omega^3 = 1$ but I was not able to make much use of this. (I played around with piecewise linear models $(x,i) \diamond (y,j) = (a_j x + b_j y, j+1)$ for $i,j \in {\bf Z}/3{\bf Z}$ and $x, y$ in some ring, as this gave six equations in six unknowns so was not overdetermined, but sadly the 906 implication was also immune to this more general model.)

[Terence Tao]

I have a partial explanation now of why the implication 906 -> 3862 is hard. One can write 906 as $L_y R_{Sx} L_y x = x$ and 3682 as $L_{L_x Sx} x = x$. From 906 we have $L_y$ is surjective, hence invertible on finite magmas. Specializing 906 we have $L_x R_{S^2 x} L_x S x = Sx = L_x x$, hence on canceling we have $R_{S^2 x} L_x Sx = x$, or equivalently $L_{L_x Sx} S^2 x = x$. On the other hand we also have $L_{L_x Sx} R_{Sx} L_{L_x Sx} x = x$, hence on canceling we have $R_{Sx} L_{L_x Sx} x = S^2 x = R_{Sx} Sx$.
Thus we can prove a weaker version of $L_{L_x Sx} x = Sx$ in which we apply $R_{Sx}$ to both sides. If right multiplication by squares is invertible then we are done, but there are models for which this is not the case, such as the $x \diamond y = \omega y$ model mentioned previously. But in any case this helped explain why the models I was trying always seemed to obey 3862.

[Terence Tao]

Another immunity that 906 -> 3862 has is to models where squaring is bijective (in particular, this gives immunity to translation invariant models). From $L_x R_{Sx} L_x x = x$ we have $L_x S^2 x = x$. Next, if we set $z := L_x S^3 x$, then $L_x z = L_x R_{S^3 x} L_x S^2 x = S^2 x$. From $L_x R_{Sz} L_x z = z = L_x S^3 x$ we have $L_{S^2 x} Sz = R_{Sz} S^2 z = S^3 x = L_{S^2 x} S^2 x$, hence $Sz = S^2 x$. If squaring is bijective, we conclude $z = S x = L_x x$. Since also $z = L_x S^3 x$, we conclude $S^3 x = x$. Now $L_x Sx = L_x z = S^2 x$, which on replacing $x$ by $S^2 x$ and using $S^3=I$ gives $L_{S^2 x} x = Sx$. This gives $L_{L_x S_x} x = Sx$, which is 3862.

[Terence Tao]

In fact the implication 906 -> 3862 is true for finite magmas! From $L_y R_{Sx} L_y x = x$ and the invertibility of $L_y$ we see that $L_y x = L_z x \implies L_y^{-1} x = L_z^{-1} x$. Iterating this we get $L_y^{-n} x = L_z^{-n} x$ for any $n \geq 1$. By finiteness, $L_y,L_z$ have a joint period, so we also have in particular $L_y^2 x = L_z^2 x$. In other words, if we have $L_y x = L_z x = w$, then also $L_y w = L_z w$.

From previous discussion we have $L_{L_x Sx} S^2 x = x = L_x S^2 x$, so by the above we have $L_{L_x Sx} x = L_x x$, which is 3862.

[Douglas McNeil]

One thing which would be good to make clear in the paper is where the finite/infinite differences in behaviour come from, even in the absence of a slick metatheorem that makes everything obvious in retrospect. Simply an overview of the recipes used to demonstrate that there are no finite counterexamples, especially when there are known infinite ones, would be useful exposition.

I mean, we've had late-entry "true for finite magmas" arguments as well as meaningful order 84 counterexamples (!), so the boundary isn't an easy one..

[Terence Tao]

I've added this as a comment to equational#924 which is a task to write the (currently only just a stub) section of the paper here.

[Matthew Bolan]

1486 does not imply 3862 or 3877!

[Douglas McNeil]

@Matthew Bolan : any particular guided magic there, or just patience and good fortune?

[Matthew Bolan]

The realization that the sporadic magmas can have many of their entries perturbed without violating 1486 made me try a very long vampire run searching for examples specifically of size 21, in the hope that the already powerful example of this order could be perturbed to something stronger.

[Matthew Bolan]

Other than that nothing fancy at all. I'm somewhat sad it violates 3862 as well as 3877, if it had only violated 3877 we would have gotten to use the twisting method to produce a degree $21^2$ counterexample to 3862.

[Matthew Bolan]

I think the instructions on finite magma explorer point one to the wrong generate_lean.py, my guess is that I'm supposed to run the one in All4x4Tables and not FinSearch. I also ran into encoding issues and had to temporarily add

encoding='utf-8'

as an argument to all the read/writes in generate_lean.py to get it to run on my machine with my version of python.

[Matthew Bolan]

equational#940

[Terence Tao]

879 does not imply 4065

[Terence Tao]

The order 12 model here comes from two basic models on 879, $i \diamond j = j+1$ on ${\bf Z}/3{\bf Z}$ and $b \diamond c = b+c$ on ${\bf Z}/2{\bf Z}$. The carrier here can be viewed as ${\bf Z}/2{\bf Z} \times {\bf Z}/2{\bf Z} \times {\bf Z}/3{\bf Z}$ with an operation of the form $(x,b,i) \diamond (y,c,j) = (x+y+f(b,c,j-i), b+c, j+1)$ for some function $f: {\bf Z}/2{\bf Z} \times {\bf Z}/2{\bf Z} \times {\bf Z}/3{\bf Z} \to {\bf Z}/2{\bf Z}$. The equation 879 reduces to the functional equation $f(b,c,i) + f(b+c,0,-i) + f(c,b+c,2-i) + f(b,b,0) = 0$, and the equation 4065 reduces to the functional equation $f(0,b,2) + f(b,b,2) = 0$. A little bit of Sudoku let me find an $f$ that obeyed 879 but not 4065, which after relabeling led to the above example.

[Terence Tao]

Oops, I just realized that this superseded @Amir Livne Bar-on 's ongoing formalization of the greedy argument for 879. Sorry...

[Matthew Bolan]

So the idea is a finite translation invariant construction? I'm amazed it's so small! I had run this particular implication through ATP for a while and got nowhere, I wonder how long it will take to find the solution if I have it search order 12.

[Terence Tao]

I'm running into the exact same encoding problem as @Matthew Bolan . A Windows thing perhaps? Where do I add the encoding='utf-8' line to the python code precisely?

[Matthew Bolan]

I did it in 4 places, everywhere it calls open()

[Terence Tao]

It's partially translation-invariant but not fully (a fully translation-invariant model would have $f(c-b, j-i)$ rather than $f(b,c,j-i)$). This model was arrived at by a very circuitious path from adapting the 1323 type models (initially without the third component with the $j+1$ shift, but I eventually worked out that the model would not work without such a shift).

[Matthew Bolan]

Alright, I remain largely unfamiliar with the translation-invariant models, I think they stopped being used around the time I showed up.

I'm very surprised that this thing exists. I can't wait to be finally done grading so that I can take a serious crack at some of these other ones.

[Terence Tao]

OK, that seemed to work. Hopefully equational#941 works

[Matthew Bolan]

Don't you need to add a line to extra.txt as well?

[Matthew Bolan]

Also since you have just resolved a conjecture from the main project I think you should modify Conjectures.lean

[Terence Tao]

Ah, forgot to hit "save" :man_facepalming:

[Terence Tao]

These sorts of models by the way were also considered by @Ibrahim Tencer (and maybe by others also), though we ended up abandoning those sorts of constructions (perhaps prematurely). In general when one has a base magma $M$ one can consider "semi-direct products" (or "extensions by cocycles") with a carrier of the form $G \times M$ and with law $(x, a) \diamond (y,b) = (x \diamond_G y + f(a,b), a \diamond_M b)$ for some function $f: M \times M \to G$, where $G$ is an abelian group or ring and $\diamond_G$ is some linear magma operation that obeys the required equational law. In order for this "semi-direct product" to obey the law we then have to solve a (linear!) functional equation on $f$ (these equations look a little bit like cocycle equations). In retrospect this could be a more broadly applicable technique, it may be worth experimenting with it more.

[Matthew Bolan]

I made equational#942 to try and correct the issues we ran into importing these counterexamples.

[Amir Livne Bar-on]

Terence Tao said:

Oops, I just realized that this superseded Amir Livne Bar-on 's ongoing formalization of the greedy argument for 879. Sorry...

A finite counter-example (with reasoning behind it!) is much better than an infinite one.

I don't remember if we have finite immunities for all the other un-formalized constructions... I'll run some searches for the older proofs

[Matthew Bolan]

We do

[Matthew Bolan]

Copying from Terry's message above, I think the remaining open finite implications are

• 677 (dual 2910). 2 implications, or 1 up to equivalence, previously established by the greedy method.
• 854 (dual 2712). 10 implications, previously established by a complicated greedy method or the unique factorization method.
• 879 (dual 2650). 2 implications, established by a (not yet formalized) greedy method.
• 906 (dual 2647), 2 implications, previously established by the greedy method.
• 1076 (dual 2531), 4 implications, established by a greedy method.
• 1110 (dual 2497), 2 implications, previously established by the confluent method.
• 1486 (dual 2126), 4 implications, previously established by the complete rewriting method.
• 1516 (dual 2091), 2 implications, previously established by a greedy method.
• 1518 (dual 2054), 8 implications, or 1 up to equivalence, previously established by the greedy method.

[Matthew Bolan]

The open 1516 implication in the finite case is different from the unformalized implication it still has, but understanding 1516's finite models may well lead to a better understanding of the law.

[Amir Livne Bar-on]

I was thinking about the main graph, that is equations 63, 713, 1289, 1323, 1516, 1692, 1729. Some of the greedy constructions were found quite early, before we started collecting "immunities" for the non-implications, so might have a counter-example.

[Matthew Bolan]

Right, but in the process of working out the finite graph we have essentially collected all of the immunities.

[Amir Livne Bar-on]

Got it, thanks

[Ibrahim Tencer]

Some notes on 1518:

I claim that in a finite 1518 model, 817 is equivalent to $S^3 = 1$ where $S$ is squaring. Proof: 817 says $x = x SSx$. We already know squaring is a bijection, so if $S^3 = 1$ we can substitute $Sy$ for $x$ and 817 becomes $Sy = Sy S^3y = Sy y$ which is just 359, which we know holds.

For the other direction, 359 says $Sx = Sx x$, so also $x = x S^{-1} x$.
So if 817 holds, we get $x S^2x = x S^{-1} x$, but then by left-cancellation $S^2x = S^{-1} x$, so $S^3x = x$.

Secondly, I've been investigating the finite models of 1518 with some help from Vampire.

There are a few classes of models. One is the linear models $x \diamond y = ax + by$, which were used as counterexamples to some implications. There are two subclasses of linear models. In the first, we have $a + b = 1$ (plus some other condition on $b$), in which case $x \diamond x = x$ and all of the consequents hold.

In the second subclass, $a = 0$ and $b^3 = 1$ so if the rightmost variable in an expression is $x$, its value is $b^n x$ where $n$ is the level of nesting of that variable, i.e. how many times it is multiplied with something. The RHS of 47, 614, and 817 all have a nesting level of 3 and the RHS of 3862 has 2, so they all hold.

We can also generalize the second class to what we can call a piecewise model: for example we take functions $f$ and $g$ with $f^3 = 1$ and $g^2 = 1$, and a subset $S$ and define

$x \diamond y = f(y)$ if $y \notin T$

$= g(y)$ if $x \notin T$ and $y \in T$

$= y$ if $x \in T$ and $y \in T$

This model will satisfy all four consequents too. (I found this one with Vampire by excluding both $x^2 = x$ and $xy = zy$.)

We can generalize this example further: take a partition $\{T_i\}$, bijections $f_{i}$, and define

$x \diamond y = f_{i}(y)$ if $x \in T_i$ and $y \in T_j$

The exact assumptions we need on the $fᵢ$'s are a bit complicated, but we can assume that $f_{i}(T_j) \subseteq T_j$ to simplify things. Then we get

$x = f_{j}f_{i}f_{j}x$

for all $x$, and this condition is sufficient to show 1518.

But this also implies that squaring has order 3, as well as $(xy)z = yz$, and $xSx = S^2x$. 47 will be true because $x(x(xx)) = f_{i}^3(x) = x$, and generally an expression in $x$ will be equal to $S^nx$ where $n$ is the nesting level, so all the consequents hold.

But it turns out there actually are models where preservation doesn't hold, e.g.

[[2, 1, 4, 5, 0, 3], [2, 3, 4, 5, 0, 1], [2, 3, 4, 1, 0, 5], [2, 3, 4, 5, 0, 1], [2, 5, 4, 3, 0, 1], [2, 3, 4, 5, 0, 1]]

$f = (024), g = (135), S = fg = gf, h_0 = (35), h_2 = (13), h_4 = (15)$

$A = \{0, 2, 4\}, B = \{1, 3, 5\}$

$xy = f(y)$ if $y \in A$, $g(y)$ if $x,y \in B$, $h_x(y)$ otherwise.

Here the partition blocks are technically 0, 2, 4, and 135, but 024 acts as a single block when it's on the right.

So far it's unclear to me whether all the consequents will hold in the more general setting.

[Ibrahim Tencer]

Come to think of it, this "model" is basically just equivalent to the original problem itself, with $L_x = f_i$ when $x \in T_i$. But maybe it can clarify some things.

[Terence Tao]

I think in general the approach of considering "piecewise" models built out of simpler base magmas is a promising one, possibly also for simplifying the three most difficult refutations 1323, 1516, 1729 in the infinite magma case as well.

For 1110, I'm thinking that a piecewise linear model such as
$(x,a) \diamond (y,b) = (\alpha x + \beta y + f(a,b), \gamma a + \delta b)$
may be promising, where $x,y, \alpha,\beta$ live in some field $F$, $\gamma,\delta,a,b$ live in another field $F'$, and $f: F' \times F' \to F$ is a function satisfying a suitable functional equation. Here the coefficients $\alpha,\beta,\gamma,\delta$ should be chosen such that $x \diamond y = \alpha x + \beta y$ and $a \diamond b = \gamma a + \delta b$ already solve 1110, for instance one choice is to take $F=F'$ and $(\alpha,\beta) = (\gamma,\delta) = (\phi,-1)$ where $\phi$ solves the golden ratio equation $\phi^2 = \phi+1$, e.g., $F = {\bf Z}/5{\bf Z}$ and $\phi = 3$, or $F = F_4 = F_2[\phi] / (\phi^2 + \phi + 1)$. When verifying 1110 for $(x,a)$ and $(y,b)$ the partial translation invariance allows one to reduce to the case $x=y=0$ and one ends up with a functional equation for $f$ that in principle can be solved by linear algebra over the field $F$. In the case $F = {\bf Z}/5{\bf Z}$ this is a linear system in 25 variables (which one can cut down to 6 or so if one assumes dilation symmetry), and for $F=F_4$ it is 16 variables, but I haven't had time to work out the details (which would lead to counterexamples of order 25 or 16 if all goes well).

One may also look for translation invariant models in groups such as $({\bf Z}/5{\bf Z})^2$ and $F_4^2 \equiv ({\bf Z}/2{\bf Z})^4$ - any such model which isn't idempotent would resolve 1110->1629. These are a bit too large for brute force search but maybe an ATP could handle it.

[Terence Tao]

For 1518, I suspect in analogy with 879 that a model of the form $(x,s,i) \diamond (y,t,j) = (ax+by+f(s,t,j-i), as+bt, j+1)$ could be successful, where $x,y,s,t$ live in some small finite field $F$ which has a linear model $x \diamond y = ax + by$ and $f: F \times F \times {\mathbf Z}/3{\mathbf Z} \to F$ is a function obeying a certain linear functional equation, but I won't have time today to try to work out the linear algebra for this.

[Matthew Bolan]

It works for 1110!

[Matthew Bolan]

I have enough to automate the process I think, can spin that up later tonight if I can finish other duties.

[Terence Tao]

Wow, that was extremely quick! What values for the parameters $\alpha,\beta,\gamma,\delta,f$ did you use?

[Matthew Bolan]

$\alpha = \gamma = \phi$, $\beta = \delta = -1$, and then $f$ I found with some lazy sage code, I think it wound up being

This

((0, 0), 1)
((0, 1), 0)
((0, 2), 0)
((0, 3), 0)
((0, 4), 0)
((1, 0), 0)
((1, 1), 0)
((1, 2), 2)
((1, 3), 4)
((1, 4), 1)
((2, 0), 3)
((2, 1), 0)
((2, 2), 2)
((2, 3), 4)
((2, 4), 4)
((3, 0), 1)
((3, 1), 1)
((3, 2), 2)
((3, 3), 4)
((3, 4), 1)
((4, 0), 4)
((4, 1), 0)
((4, 2), 2)
((4, 3), 3)
((4, 4), 1)

but I had to do a little parsing to print that, which maybe I did incorrectly.

[Matthew Bolan]

It found a 6 dimensional space of functions $f$ satisfying the needed equation. There are some obvious linear dependencies in the system (for example the functional equation is trivial at $((0,0),(0,0))$)

[Terence Tao]

That's a reassuringly large space of examples. (Though there are some trivial "coboundary" solutions $f(a,b) = \alpha g(a) + \beta g(b) - g(\gamma a + \delta b)$ that may be occupying much of this space.) It gives hope that the method should be useful for many of the other outstanding equations (though I expect it won't work for 854, as the functional equation now has three variables and the linear system is likely to be extremely overdetermined).

[Terence Tao]

A side remark: it seems we have stumbled upon some sort of "magma cohomology" that is a variant of group cohomology. I don't think we have enough people with the required background to explore this further for this project, but it might be something to note in the paper for future research. [ADDED: and it would finally provide a use case in our project for Magma, which has been a surprisingly absent software package so far!]

[Matthew Bolan]

Yes, I am reminded of the old joke that elementary school arithmetic is arithmetic in $\mathbb Z / 10 \mathbb Z$ twisted by cocycles

[Matthew Bolan]

I'd like to say that this construction gives us an extension $G \hookrightarrow G \rtimes M  \twoheadrightarrow M$, but to define the first map I want $M$ to have a pointed idempotent $0$ with $f(0,0)$ the identity in $G$.

[Terence Tao]

It may be better to view the extension as a principal $G$-bundle over $M$, so that one has a translation action of $G$ rather than an embedding.

[Matthew Bolan]

Ok I think I have it at least somewhat automated. It found an order $13^2$ counterexample to the remaining 1076 implications.

[Matthew Bolan]

Not yet run all the others, I made some poor design decisions. With the very large tables we probably need to do better than just giving lean the table.

[Matthew Bolan]

refute1076to2294and4435.txt

[Matthew Bolan]

Let me modify it to print $f$, and then I'll try at least the other two variable equations.

[Douglas McNeil]

854 does not imply 413.

https://teorth.github.io/equational_theories/fme/?magma=5%2011%200%2011%200%200%2014%2013%200%200%2018%203%200%2014%206%2013%2014%200%2013%0A5%2011%201%205%201%201%204%201%201%201%204%201%201%2017%201%201%2017%201%201%0A2%202%207%202%208%204%204%202%204%208%202%208%207%202%202%202%2017%204%208%0A5%2011%203%205%203%203%209%203%203%203%2018%203%203%205%203%203%205%203%203%0A4%204%207%204%2014%204%204%204%204%208%204%208%207%204%204%204%2017%204%208%0A5%205%201%205%205%204%204%205%201%205%205%205%207%205%205%205%205%207%205%0A5%205%2010%205%206%2010%204%206%201%206%205%206%2010%205%206%206%205%201%206%0A8%207%207%207%207%207%207%2013%207%207%207%208%207%207%208%2013%207%207%208%0A8%208%201%208%208%204%204%208%201%208%208%208%2015%208%208%208%208%2015%208%0A9%209%207%209%2014%209%209%209%209%208%209%208%207%209%209%209%208%209%208%0A5%2011%2010%2011%2010%2010%209%2010%2010%2010%2014%203%2010%2017%2010%2010%205%2010%2010%0A9%2011%200%2011%200%2011%2018%2016%2011%200%2018%208%200%2018%2016%2016%2014%2011%2013%0A12%2012%207%2012%208%204%204%2012%204%208%2012%208%207%2012%2012%2012%208%204%208%0A5%2011%2013%2011%2013%2013%204%2013%2013%2013%209%203%2013%2017%2013%2013%2017%2013%2013%0A5%2014%2014%2014%2014%2014%2014%2013%2014%2014%2014%208%2014%2014%205%2013%2014%2014%208%0A5%2015%2015%2015%2015%2015%2015%2013%2015%2015%2015%208%2015%2015%205%209%2015%2015%205%0A9%2011%2013%2011%2013%2016%209%2016%2016%2013%209%203%2013%209%2016%2016%2017%2016%2013%0A17%2017%201%2017%2017%204%204%2017%201%2017%2017%2017%2015%2017%2017%2017%2017%2015%2017%0A9%2018%207%2018%207%2018%2018%209%2018%207%2018%208%207%2018%209%209%207%2018%208%0A

:smiling_face_with_tear:

[Matthew Bolan]

How was that one found?

[Matthew Bolan]

Matthew Bolan said:

refute1076to2294and4435.txt

This is built up from two copies of $5x+9y \pmod {13}$ and has f

equal to this

((0, 0), 0)
((0, 1), 0)
((0, 2), 0)
((0, 3), 4)
((0, 4), 4)
((0, 5), 3)
((0, 6), 2)
((0, 7), 9)
((0, 8), 4)
((0, 9), 0)
((0, 10), 2)
((0, 11), 0)
((0, 12), 0)
((1, 0), 1)
((1, 1), 0)
((1, 2), 0)
((1, 3), 0)
((1, 4), 1)
((1, 5), 12)
((1, 6), 3)
((1, 7), 0)
((1, 8), 4)
((1, 9), 0)
((1, 10), 7)
((1, 11), 0)
((1, 12), 0)
((2, 0), 0)
((2, 1), 0)
((2, 2), 0)
((2, 3), 9)
((2, 4), 0)
((2, 5), 2)
((2, 6), 2)
((2, 7), 5)
((2, 8), 6)
((2, 9), 5)
((2, 10), 4)
((2, 11), 12)
((2, 12), 10)
((3, 0), 0)
((3, 1), 0)
((3, 2), 0)
((3, 3), 0)
((3, 4), 12)
((3, 5), 2)
((3, 6), 1)
((3, 7), 4)
((3, 8), 10)
((3, 9), 5)
((3, 10), 0)
((3, 11), 0)
((3, 12), 12)
((4, 0), 0)
((4, 1), 0)
((4, 2), 0)
((4, 3), 1)
((4, 4), 0)
((4, 5), 12)
((4, 6), 9)
((4, 7), 0)
((4, 8), 6)
((4, 9), 0)
((4, 10), 7)
((4, 11), 0)
((4, 12), 7)
((5, 0), 0)
((5, 1), 0)
((5, 2), 0)
((5, 3), 3)
((5, 4), 11)
((5, 5), 0)
((5, 6), 1)
((5, 7), 7)
((5, 8), 2)
((5, 9), 5)
((5, 10), 3)
((5, 11), 10)
((5, 12), 0)
((6, 0), 0)
((6, 1), 0)
((6, 2), 9)
((6, 3), 12)
((6, 4), 11)
((6, 5), 1)
((6, 6), 0)
((6, 7), 0)
((6, 8), 11)
((6, 9), 10)
((6, 10), 5)
((6, 11), 12)
((6, 12), 6)
((7, 0), 0)
((7, 1), 0)
((7, 2), 0)
((7, 3), 11)
((7, 4), 3)
((7, 5), 6)
((7, 6), 4)
((7, 7), 0)
((7, 8), 12)
((7, 9), 8)
((7, 10), 3)
((7, 11), 3)
((7, 12), 12)
((8, 0), 0)
((8, 1), 0)
((8, 2), 0)
((8, 3), 10)
((8, 4), 1)
((8, 5), 6)
((8, 6), 10)
((8, 7), 1)
((8, 8), 0)
((8, 9), 2)
((8, 10), 0)
((8, 11), 1)
((8, 12), 6)
((9, 0), 0)
((9, 1), 0)
((9, 2), 0)
((9, 3), 3)
((9, 4), 12)
((9, 5), 3)
((9, 6), 0)
((9, 7), 11)
((9, 8), 2)
((9, 9), 0)
((9, 10), 3)
((9, 11), 8)
((9, 12), 1)
((10, 0), 0)
((10, 1), 0)
((10, 2), 12)
((10, 3), 4)
((10, 4), 2)
((10, 5), 9)
((10, 6), 11)
((10, 7), 0)
((10, 8), 11)
((10, 9), 9)
((10, 10), 0)
((10, 11), 8)
((10, 12), 9)
((11, 0), 0)
((11, 1), 0)
((11, 2), 12)
((11, 3), 5)
((11, 4), 1)
((11, 5), 6)
((11, 6), 9)
((11, 7), 8)
((11, 8), 9)
((11, 9), 9)
((11, 10), 3)
((11, 11), 0)
((11, 12), 11)
((12, 0), 0)
((12, 1), 0)
((12, 2), 12)
((12, 3), 6)
((12, 4), 8)
((12, 5), 11)
((12, 6), 10)
((12, 7), 5)
((12, 8), 4)
((12, 9), 8)
((12, 10), 6)
((12, 11), 11)
((12, 12), 0)

[Matthew Bolan]

1516 does not imply 1489, with a degree $7^2$ counterexample.

[Matthew Bolan]

1516not1489.txt

[Matthew Bolan]

677 and 1518 seem more resilient than the others, and the fact 854 is three variables means I'll have to refactor the code to try it, but it also means the method is less likely to work.

[Douglas McNeil]

I started with one of the 854 with 4 10 violations that I grew back when we thought they'd be easy to find and that having a bunch of 10 violations would be helpful. Then I threw away different fractions of the cells, and grew it up to 19, and lucked out.

This brings me up to 3 useful finite magma in total over the course of the project, or about as many as you've found in the last few minutes. :joy_cat: But I'll take what I can get! :-)

[Douglas McNeil]

And I think you're right about large tables: we still have Terence's order 84 counterexample we squashed down to 50. More cleverness might equal more compression, but ideally Lean shouldn't be taking 10+ seconds.

[Matthew Bolan]

you can definitely PR yours though.

[Douglas McNeil]

854 does not imply 3316 or 3925.

https://teorth.github.io/equational_theories/fme/?magma=5%2011%2018%205%200%200%2011%206%200%200%2011%2013%203%2011%206%205%2015%2013%209%2014%201%0A5%204%201%204%201%201%204%201%201%201%204%201%201%205%201%204%201%201%204%2014%201%0A2%202%207%202%208%204%204%202%204%208%202%208%207%202%202%202%207%2019%202%204%204%0A5%2011%203%205%203%203%2011%2010%203%203%2011%2010%203%2011%2010%209%203%2010%209%2014%201%0A4%204%207%204%207%204%204%204%204%208%204%208%207%204%204%204%207%2013%204%204%204%0A5%205%207%205%205%204%204%205%201%205%205%205%207%205%205%205%201%205%205%2014%2010%0A5%205%201%205%206%201%204%206%201%206%205%206%201%205%206%205%201%206%205%2014%2010%0A8%207%207%208%207%207%207%2010%207%207%207%208%207%207%209%208%207%201%209%207%2010%0A8%208%207%208%208%204%204%208%2010%208%208%208%201%208%208%208%2010%208%208%2014%2010%0A9%209%207%209%207%209%209%209%209%208%209%208%207%209%209%209%207%2013%209%209%209%0A5%204%2010%205%2010%2010%204%2010%2010%2010%204%2010%2010%205%2010%204%2010%2010%204%2014%2010%0A9%2011%207%209%207%2011%2011%209%2011%207%2011%208%207%2011%209%209%207%2013%209%2011%209%0A12%2012%207%2012%2020%204%204%2012%204%208%2012%208%207%2012%2012%2012%207%208%2012%2017%204%0A5%204%2013%205%2013%2013%204%2013%2013%2013%204%2013%2013%205%2013%205%2013%2013%209%2014%2013%0A8%2014%2014%209%2014%2014%2014%2013%2014%2014%2014%208%2014%2014%209%209%2014%2010%209%2014%201%0A5%2011%2015%205%2015%2015%2011%201%2015%2015%2011%2010%2015%2011%201%209%2015%2010%209%2014%2010%0A2%2016%207%202%2020%2017%204%2016%2017%2019%2016%208%207%2016%2016%202%207%208%202%2017%204%0A9%2017%207%209%207%2017%2017%209%2017%200%2017%208%207%2017%209%209%207%2013%209%2017%209%0A5%2011%2018%205%2018%2018%2014%201%2018%2018%2011%206%2018%2011%201%205%2018%201%209%2014%201%0A5%205%2010%205%2019%2010%204%2019%2010%2019%205%2019%2010%205%2019%205%2010%2019%205%2014%2010%0A5%2020%2018%205%2020%2017%2014%206%2018%2020%2020%205%2018%2020%206%205%207%205%205%207%2010%0A

[Matthew Bolan]

Quitting for the night. I could not get Terry's idea of taking $G$ to be the direct sum of a linear magma and the order 3 magma he mentions to work for 1518, but bugs are always a possibility. I also tried a few small magmas for $G$ which have been used in the past to falsify implications from 677 or 1518, with no luck. Most of my search was in the case where $M=G$ is a linear magma of prime order < 50, and I haven't tried fields which aren't of prime order yet.

[Jose Brox]

Which implications remain open now?

[Terence Tao]

@Matthew Bolan is keeping score at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/484845205 . Two implications associated to 677, eight associated to 1518, and now just four for 854 (previously ten). For some reason 854 has a tradition of being taken out in chunks, while all the other equations seem to be all-or-nothing affairs...

[Matthew Bolan]

Well, 1055 implies 1045, so what remains of 854 is an all or nothing affair

[Vlad Tsyrklevich]

Wow! A flood of progress in the past few days.

[Matthew Bolan]

Is the order 169 example a record? I seem to remember some large linear magmas in the Higman-Neumann project.

[Vlad Tsyrklevich]

I don't think there has been anything over order 100 there or anywhere else.I stand corrected.

[Matthew Bolan]

https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Higman-Neumann.20characterization.20of.20groups/near/483137635

[Jose Brox]

Terence Tao ha dicho:

@Matthew Bolan is keeping score at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/484845205 . Two implications associated to 677,

In the Equation Explorer (finite graph option), for 677 I only see 1 implication remaining, to 255. Similarly, for 854, once we remove 3316 and 3925, I only see 3 implications remaining, to 413, 1045 and 1055.

[Vlad Tsyrklevich]

These are all dual reduced. e.g. 677 and the implication by its dual

[Matthew Bolan]

Also, 854 -> 413 has been resolved (By Douglas, just above).

[Matthew Bolan]

The new magmas still need to be put into lean, but I refrained from just making the usual PR because of the size of the order 169 and 49 examples (though Douglas's examples are small enough they definitely can just be added). Luckily the magmas still have a simple description for now, but probably this is what should be formalized.

In general, what is our threshhold for adding a finite magma directly?

[Vlad Tsyrklevich]

I'm not sure, I think if it compiles then it's fine to upstream. If it would require special handling (e.g. increasing the maxHeartbeats required for Lean to finish), then perhaps it's worth looking for smaller alternatives, though that seems fine to leave as a conjecture.

[Vlad Tsyrklevich]

Douglas McNeil said:

I started with one of the 854 with 4 10 violations that I grew

I wasn't following along back then, what method did you use to do this? I guess to be specific, what software and how did you use it?

[Jose Brox]

Terence Tao ha dicho:

and it would finally provide a use case in our project for Magma

(Just for the record, I have been using Sage for computing linear and *-linear models).

[Douglas McNeil]

I wasn't following along back then, what method did you use to do this? I guess to be specific, what software and how did you use it?

So IIRC we had the order 12 magma that was 854+1 10 viol (sorry, can't remember who to credit!) with a reduced order 11 version. I wrote manual Python code to perturb the 854 magma, changing and deleting values, and sometimes imposing the necessary fixes myself, but the main driver was feeding it to kissat as an SAT problem where only the new values were free and I asked it to extend it in an 854-compatible way. This eventually got me the second 10 violation, and ultimately an indefinite number of them, but didn't seem to be getting me any closer to a 413 violation.

What I did yesterday was start with my 854 with 4 10 violations magma, generate vampire code fixing some fraction of the values taken from that magma, and use the same vampire -sa fmb -fmbss {size} command that MB had found so fruitful.

Side note: I guess I've had my own version of the bitter lesson. At the time, when I was hoping to rule out 413 violations, I also wrote some unsuccessful C++ code to start with every possible primitive 413 violation and grow every possible 854 magma, hoping they'd all fail. It managed to eliminate a lot of them, but there were 25% that were sticky. I also had my own equivalent of discovering how important the mace4 parameters were, because the code's performance changed by orders of magnitude depending on the strategy I used to pick the next empty cell to try to force.

But once the infinite counterexample was found it showed my approach wouldn't work like I wanted. The bitter lesson is this: doing the same "rule out every 413-violating seed as compatible with 854" but doing it using vampire instead of custom code was not only much easier, it managed to rule out all but 4 or 5 in no time. :man_shrugging:

[Vlad Tsyrklevich]

And since I haven't tried to do something like this myself and I'm curious, what does feeding a partially completed magma to vampire look like? Like, what is the TPTP?

[Douglas McNeil]

Pretty much what you'd guess, TBH. Here's what I used:

TPTP code

fof(equation854, axiom, (! [X,Y,Z] : X = magma(X, magma(magma(Y, Z), magma(X, Z))))).

fof(elements, axiom, (0 != 1 & 0 != 2 & 0 != 3 & 0 != 4 & 0 != 5 & 0 != 6 & 0 != 7 & 0 != 8 & 0 != 9 & 0 != 10 & 0 != 11 & 0 != 12 & 0 != 1
3 & 0 != 14 & 0 != 15 & 1 != 2 & 1 != 3 & 1 != 4 & 1 != 5 & 1 != 6 & 1 != 7 & 1 != 8 & 1 != 9 & 1 != 10 & 1 != 11 & 1 != 12 & 1 != 13 & 1 !
= 14 & 1 != 15 & 2 != 3 & 2 != 4 & 2 != 5 & 2 != 6 & 2 != 7 & 2 != 8 & 2 != 9 & 2 != 10 & 2 != 11 & 2 != 12 & 2 != 13 & 2 != 14 & 2 != 15 &
3 != 4 & 3 != 5 & 3 != 6 & 3 != 7 & 3 != 8 & 3 != 9 & 3 != 10 & 3 != 11 & 3 != 12 & 3 != 13 & 3 != 14 & 3 != 15 & 4 != 5 & 4 != 6 & 4 != 7
& 4 != 8 & 4 != 9 & 4 != 10 & 4 != 11 & 4 != 12 & 4 != 13 & 4 != 14 & 4 != 15 & 5 != 6 & 5 != 7 & 5 != 8 & 5 != 9 & 5 != 10 & 5 != 11 & 5
!= 12 & 5 != 13 & 5 != 14 & 5 != 15 & 6 != 7 & 6 != 8 & 6 != 9 & 6 != 10 & 6 != 11 & 6 != 12 & 6 != 13 & 6 != 14 & 6 != 15 & 7 != 8 & 7 !=
9 & 7 != 10 & 7 != 11 & 7 != 12 & 7 != 13 & 7 != 14 & 7 != 15 & 8 != 9 & 8 != 10 & 8 != 11 & 8 != 12 & 8 != 13 & 8 != 14 & 8 != 15 & 9 != 1
0 & 9 != 11 & 9 != 12 & 9 != 13 & 9 != 14 & 9 != 15 & 10 != 11 & 10 != 12 & 10 != 13 & 10 != 14 & 10 != 15 & 11 != 12 & 11 != 13 & 11 != 14
& 11 != 15 & 12 != 13 & 12 != 14 & 12 != 15 & 13 != 14 & 13 != 15 & 14 != 15)).

fof(magma_known, axiom, (magma(0,14) = 6 & magma(1,5) = 1 & magma(1,10) = 4 & magma(2,12) = 7 & magma(2,14) = 2 & magma(3,1) = 11 & magma(3
,2) = 3 & magma(3,5) = 3 & magma(4,2) = 7 & magma(4,3) = 4 & magma(4,9) = 8 & magma(4,11) = 8 & magma(4,14) = 4 & magma(5,0) = 5 & magma(5,
5) = 4 & magma(5,9) = 5 & magma(5,11) = 5 & magma(5,12) = 7 & magma(5,14) = 5 & magma(6,0) = 5 & magma(6,2) = 10 & magma(6,4) = 6 & magma(6
,5) = 10 & magma(6,6) = 4 & magma(6,11) = 6 & magma(7,1) = 7 & magma(7,10) = 7 & magma(7,12) = 7 & magma(8,4) = 8 & magma(8,13) = 8 & magma
(9,2) = 7 & magma(9,3) = 9 & magma(9,8) = 9 & magma(9,9) = 8 & magma(9,13) = 9 & magma(11,1) = 11 & magma(11,5) = 11 & magma(12,3) = 12 & m
agma(12,5) = 4 & magma(12,8) = 4 & magma(12,12) = 7 & magma(12,13) = 12 & magma(13,6) = 4 & magma(14,4) = 14 & magma(14,11) = 8 & magma(14,
13) = 14 & magma(15,15) = 9)).

fof(eq413, conjecture, (X = magma(X, magma(X, magma(X, magma(Y, X)))))).

I use the same toolset to generate vampire & mace4 code, and I can't remember which of them needs the distinctness condition and which one doesn't, so I always toss it in. (Got my hopes up once when searching for a version of something, only to discover that the matrix was large but still trivial..)

[Matthew Bolan]

Douglas, do you mind if I make the PR to add your 854 magmas?

[Douglas McNeil]

No, please go ahead-- the last time I did it I got the order of ops wrong, and if memory serves you just had to sort out the process the other day anyhow so if you're up for it I'm sure it'll be more efficient. Thanks!

[Matthew Bolan]

Ok, its at equational#951

[Terence Tao]

I agree with Vlad's criterion (compiles in Lean without extra heartbeats or other parameter changes); there are edge cases where one could argue that the criterion is too restrictive or too permissions, but it is at least a clear rule.

For the order N^2 examples with N=7,13, the structure of the cohomological construction is such that the law can be verified with O(N^2) calculations rather than O(N^4) (basically, one can set the first coordinates of x,y equal to zero for free, due to the partial translation symmetry). So it should be possible to verify them in Lean within the heartbeat limit, after one sets up some API for magma extensions and a criterion for verification, which can then be applied to the three examples we have so far (plus the small order 12 example, though that one already made it into the Lean codebase). [EDIT: I wrote a blueprint chapter to try to formalize the cohomology construction in more abstract language, which could potentially be helpful for such an API.]

@Matthew Bolan : it's a shame that none of the outstanding implications for 1518 fell to the product choice for G. Just as a sanity check, does your code recover the order 12 example for 879, which uses this construction?

[Matthew Bolan]

Yes.

[Matthew Bolan]

At least, it finds this one, unsure if this is exactly the same as yours

[Terence Tao]

Well, there's a whole linear space of examples (minus a subspace that accidentally obeys 4065), so probably not identical, but still, that is confirmation that 1518 has some real resistance and this isn't just a coding artefact. It surprises me slightly - I view 1518 and 879 as being quite similar in structure - but perhaps sometimes the linear algebra just doesn't work out. (Cohomology is a famously subtle subject.)

[Terence Tao]

For 1518, one can also take $G$ to be a right-absorptive model $x \diamond y = y$, so the model is now of the form $(x,a) \diamond (y,b) = (y + f(a,b), a \diamond b)$. Then I think the cocycle equation is $f(b,a) + f(a, b \diamond a) + f(Sb, a \diamond (b \diamond a)) = 0$ and one could take $G$ to be the free abelian group generated by the $f(a,b)$ subject to these relations. One could then try setting $M$ to the various models described by @Ibrahim Tencer and hope for a hit.

[Matthew Bolan]

I think you may have swapped the roles of $G,M$ compared to the blueprint, is that right? I think my code already checks right-absorptive models for $M$ as they are linear, and I've already tried a few of Ibrahim's models for $G$.

[Matthew Bolan]

I intend to eventually support all finitely generated abelian groups for $M$, but currently I cannot as sage does not seem to have good support for linear algebra in these groups, so I'll have to roll my own.

[Terence Tao]

Sorry for the confusion. Yes, in the blueprint I swapped the notation to conform to more standard group cohomology language; I'll try to use those conventions more consistently going forward.

[Matthew Bolan]

By the way, I don't see an obstacle to taking the multiplication on $M$ to be $x \diamond y = ax+by+c$, but I'm not at home to test it anymore

[Terence Tao]

Yes, one could consider this more general model, though I think it doesn't add much generality (one can largely absorb the $c$ into the cocycle $f$.

I now understand why 1518 is harder than 879: as @Ibrahim Tencer already observed the non-shift linear models for 1518 are idempotent, whereas for 879 they are non-idempotent. This is relevant because all the outstanding implications are 1-variable equations so without loss of generality we can restrict ourselves to magmas generated by one generator, which means that the base magma $G$ can also be taken to be generated by one generator. But idempotent magmas then become useless because every element only generates itself. So we really only have one useful base magma for 1518 right now, namely the shift $x \mapsto x+1$ on ${\mathbb Z}/3{\mathbb Z}$; multiplying this base with other linear models doesn't accomplish anything. This indicates that we should somehow look for more candidate base magmas that are non-idempotent and generated by a single element than just the ${\mathbb Z}/3{\mathbb Z}$ shift. So presumably Ibrahim's piecewise models are a place to start...

[Pace Nielsen]

I don't know if this is helpful or not, but working with Equation 677, the solutions over a generic field to a linear model $x\diamond y=\alpha x + \beta y$ come in two flavors. Type 1: $\beta$ is a primitive 5th root of unity (i.e. a root of $x^4+x^3+x^2+x+1$) and $\alpha=1-\beta$. Type 2: $\beta$ is a root of $x^4+x^3+2x^2+2x+1$ and $\alpha=-\beta^3-\beta-1$.

[Terence Tao]

Hmm, for 1518, if one assumes all of the unproved consequents 47, 614, 817, 3862, I think the only nontrivial model generated by a single generator is the cyclic shift model $x \diamond y = y+1$ on ${\mathbf Z}/3{\mathbf Z}$ (up to isomorphism), which means that we're stuck with that as our only option for base model unfortunately.

[Terence Tao]

@Pace Nielsen Now that I see the importance of non-idempotence for the base models, I would say that the Type 2 models you listed would be more useful for the base than the Type 1 models. As for the range... I think there is some advantage to having the range be similar to the base in some ways. Otherwise one would expect to encounter "Goursat lemma" or "Schur-Zassenhaus" type obstructions to having interesting extensions.

[Matthew Bolan]

Small observation, but due to the fact 1518 -> 359, we have 1518 -> 47 if and only if 1518 -> 614. Prover 9 also tells me if 1518 -> 3862, then all 4 implications are true.

[Pace Nielsen]

@Terence Tao Although you already worked out that the cyclic shift model is the only nontrivial base model of interest for 1518, I figured it wouldn't hurt to work it out a slightly different way.

The linear models where $x\diamond y = \alpha x + \beta y$ (with $\alpha,\beta$ in some ring) have coefficients satisfying

$$\beta\alpha=\alpha\beta=-\alpha^2+\alpha,\qquad \alpha^3=2\alpha^2-2\alpha,\qquad \beta^3=\alpha^2-\alpha+1.$$

In an integral domain, either $\alpha=0$ and $\beta$ is cube root of unity (giving the cyclic shift model [multiplicatively], as well as the trivial "choose the right entry" model), or $\beta=1-\alpha$ and $\alpha$ is a root of $x^2-2x+2$ (giving an idempotent model). By the Chinese remainder theorem, we know that the generic case is essentially the direct product of these two cases.

Changing to the slightly more complicated model $x\diamond y=\alpha x+\beta y + \gamma$ leads to the additional relations

$$(\beta^2+\beta+1)\gamma=0,\qquad \alpha\gamma=0.$$

So, in an integral domain, either $\gamma=0$ (and nothing changes) or we are back in the shift model, but with an extra arbitrary additive shift. But that is just isomorphic (as you mentioned) to the original shift model.

[Jose Brox]

Terence Tao ha dicho:

3682

(It actually is 3862, I was going mad because 3682 is just $xx=(yx)(zz)$ and is not implied by $xy=y$, while 1518 is :big_smile:)

[Douglas McNeil]

854 does not imply 1045 or 1055: I think my work here is done. :joy_cat:

https://teorth.github.io/equational_theories/fme/?magma=5%2011%200%2011%200%200%2014%2013%200%200%2014%203%200%2014%2013%2013%2014%200%2013%2021%2014%2019%2019%200%0A5%2011%201%2017%201%201%204%201%201%201%205%201%201%205%201%201%205%201%201%2021%2014%2019%2019%201%0A2%202%207%202%208%204%204%202%204%208%202%208%207%202%202%202%2017%204%208%202%202%2017%2017%2022%0A5%2011%203%205%203%203%204%203%203%203%2014%203%203%205%203%203%205%203%203%2021%2014%2019%2019%203%0A4%204%207%204%207%204%204%204%204%208%204%208%200%204%204%204%208%204%208%2021%204%2019%2019%204%0A5%205%2020%205%205%204%207%205%201%205%205%205%2020%205%205%205%205%2015%205%205%202%205%205%2022%0A5%205%2020%205%206%201%2015%206%201%206%205%206%2020%205%206%206%205%201%206%206%202%205%205%2022%0A8%207%207%207%207%207%207%2013%207%207%207%2023%207%207%208%209%207%207%2023%208%207%207%207%207%0A8%208%2020%208%208%204%204%208%201%208%208%208%2020%208%208%208%208%2015%208%208%202%208%208%2022%0A9%209%207%209%2014%209%209%209%209%208%209%208%2014%209%209%209%208%209%208%2021%209%2019%2019%209%0A5%2011%2010%2011%2010%2010%204%2010%2010%2010%2014%203%2010%205%2010%2010%205%2010%2010%2021%2015%2019%2019%2010%0A9%2011%200%2011%200%2011%2018%2016%2011%200%2018%208%200%2018%2016%2016%2014%2011%2013%2021%2018%2019%2019%2011%0A12%2012%207%2012%208%204%204%2012%204%208%2012%208%2020%2012%2012%2012%208%204%208%2012%2012%2017%208%2022%0A5%2011%2013%2011%2013%2013%204%2013%2013%2013%209%203%2013%2017%2013%2013%2017%2013%2013%2021%2015%2019%2019%2013%0A8%2014%2014%2014%2014%2014%2014%2013%2014%2014%2014%2023%2014%2014%205%209%2014%2014%2023%205%2014%2014%2014%2014%0A8%2015%2015%2015%2015%2015%2015%2013%2015%2015%2015%208%2015%2015%208%209%2015%2015%205%208%2015%2015%2015%2015%0A9%2011%2013%2011%2013%2016%209%2016%2016%2013%209%203%2013%209%2016%2016%2017%2016%2013%2021%202%2019%2019%2016%0A17%2017%2020%2017%2017%204%204%2017%201%2017%2017%2017%2020%2017%2017%2017%2017%2015%2017%2017%202%2017%2017%2022%0A9%2018%207%2018%207%2018%2018%209%2018%207%2018%208%207%2018%209%209%207%2018%208%2021%2018%2019%2019%2018%0A9%2011%200%2011%200%2019%2018%2016%2019%200%2018%203%200%2018%2016%2016%2014%2019%2013%2023%2018%2019%2019%2019%0A5%2017%2020%2017%2020%201%2015%2020%201%2020%2017%2020%2020%2017%2020%2020%2017%201%2020%2020%2015%2017%2017%2022%0A9%2011%200%2011%200%2021%2018%2021%2021%2013%2018%203%200%209%2021%2021%2017%2021%2013%2021%2018%2017%2019%2021%0A4%2011%200%2011%2013%2022%204%2022%2022%2013%209%203%200%209%2022%2022%2017%2022%2013%2022%2018%2017%2019%2022%0A23%2023%2020%2023%2023%204%204%2023%201%2023%2023%2023%2020%2023%2023%2023%2023%2015%2023%2023%202%2023%2023%2022

[Ibrahim Tencer]

As for why 1518 tends to imply that $S^3 = 1$ (equivalent to 817): The main obstacle is that for many elements we tend to have $xy = Sy$. So let's say that $x < y$ if this occurs. Then, if $y < x$, $x < Sx$, and $Sy < S^2x$, from 1518 we get $S^3x = x$.
Since $x < x$ it's enough to show that $x < Sx$ ($x Sx = SSx$) and $Sx < SSx$. Notice that 359 says $Sx < x$, 3862 says $xSx < x$, and 4065 (another known consequence of 1518) says $Sxx < x$. So somehow we are trying to flip 359 and 4065 around, but the relation is not symmetric in general (as in the above piecewise magma).

The equation $x < Sx$ (call it the "elevation law" for short -- not sure how to check what the number of this one is) holds in all the model classes above. And it's extremely fast for Vampire to check, I verified that it holds up to order 37 before apparently running out of memory. Notice that it has 5 operations so it's not one of the original list. What's more, if two laws out of {47, 817, $x < Sx$} hold (in the presence of 359), then the third does too.

It also suffices that $x < Sx$ and that S preserves <. And S preserves < if S is a homomorphism. S is a homomorphism in the linear models but it may or may not be in the piecewise models.

We can also use elevation to show that if 47 and 817 hold in a 1518 model then so does 3862:

Suppose $Sy = x$, then $(x Sx) x = SSx x = y Sy = SSy = Sx$.

So if 1518 implies 47 and 817 it also implies 3862. So 47 and 817 are sufficient to show that the magma generated by a single element is just $\{x, Sx, SSx\}$ with the shift law.

Matthew Bolan said:

Small observation, but due to the fact 1518 -> 359, we have 1518 -> 47 if and only if 1518 -> 614. Prover 9 also tells me if 1518 -> 3862, then all 4 implications are true.

Interesting, did it produce a human-readable proof? This would mean showing 47+817 and showing 3862 are equivalent.

[Ibrahim Tencer]

In a 1518 magma for any $y$ we have $Sy = Sy(Sy(ySy))$. If we have the elevation law ($xSx = SSx$) then $Sy = Sy(Sy(SSy))$. So by 359, $Sy(Sy(SSy)) = Sy y$, and canceling we get $y = Sy SSy$, but then $y = SSSy$ by elevation. So actually the elevation law implies 817 in any *finite 1518 model, hence it also implies 47, which means it implies 3862.

[Ibrahim Tencer]

(before I had said any 1518 model but we do need left-cancellation, so it will hold in finite models in particular)

[Vlad Tsyrklevich]

Douglas McNeil said:

854 does not imply 1045 or 1055

I have created equational#957

[Terence Tao]

Douglas McNeil said:

854 does not imply 1045 or 1055: I think my work here is done. :joy_cat:

Congrats! Can you share a bit about how you found this example?

I think now one can safely comment out Equation854.lean from ManuallyProven.lean as the various infinitary arguments previously used to establish refutations from 854 are now superseded by the finite ones, which may shave a few seconds off the Lean compilation. I'm going to try this now to test the theory.

[Terence Tao]

@Ibrahim Tencer based on your analysis, I wonder if one could ask an ATP whether the refutations from 1518 remain open if one additionally assumes that (a) $S$ and $L_y$ are bijections (this is automatic from finiteness, but one may need to give it to the ATP explicitly), (b) $S$ is a homomorphism; (c) $S^6 = 1$; and (d) existence of a homomorphism to the ${\mathbb Z}/3{\mathbb Z}$ cyclic shift. If we can assume all these things without accidentally getting the implications, this may help guide us to building a counterexample (maybe with more ATP calculations).

[Mario Carneiro]

Terence Tao said:

I think now one can safely comment out Equation854.lean from ManuallyProven.lean as the various infinitary arguments previously used to establish refutations from 854 are now superseded by the finite ones, which may shave a few seconds off the Lean compilation. I'm going to try this now to test the theory.

my general intuition is the opposite, large finite calculations are harder for lean than small seeds plus abstract nonsense

[Douglas McNeil]

@Terence Tao : Same technique as worked for my other recent 854 refutations: start with a magma with a lot of 10 violations, and in this case I used the the 413 refutation as a seed (so the 1045/55 refutation actually handles the 413 as well, I didn't lose it). Perform a bunch of runs removing random fractions of that magma, in the hopes that we keep the refutation-promoting parts while losing the portions of the magma which might be constraining us too tightly and either force or strongly coerce us into respecting the law we're trying to violate. Probably this could be done more cleverly, but since I don't know exactly what's causing what, might as well do it randomly and let the automation handle it (a "sweet" approach as opposed to a "bitter" one, I guess. :stuck_out_tongue_wink:)

Also letting the magma grow a few orders is likely important, it feels like the additional degrees of freedom give the construction more room to breathe, without requiring you to have hit exactly the right arrangement to begin with.

Basically it all comes down to something you said (which I might even be misremembering!) about needing not one but two 10 violations to show something or other 854-related, which led me to want to have a lot of them around.

Also, I looked it up, and if I'm reading right it was @Daniel Weber who found the original order 12 854 magma with the 10 violation, and everything I've found (even this order 24 one!) is ultimately downstream of that magma, however disguised it might seem.

[Terence Tao]

Mario Carneiro said:

Terence Tao said:

I think now one can safely comment out Equation854.lean from ManuallyProven.lean as the various infinitary arguments previously used to establish refutations from 854 are now superseded by the finite ones, which may shave a few seconds off the Lean compilation. I'm going to try this now to test the theory.

my general intuition is the opposite, large finite calculations are harder for lean than small seeds plus abstract nonsense

For head-to-head comparisons, I would agree. Though currently, because the equational theories project is interested in completing both the infinite magma graph and the finite magma graph, we are going to need the finite counterexamples anyway, so commenting out the infinitary arguments seems like a no-brainer to me. (Also, it is possible with some further optimization of the finite counterexample planner that some of the new finite examples can be used to remove some of the older ones, so the net performance cost may eventually go down slightly.) Though I see that the CI for updating the Lean codebase is now pretty fast (for my most recent commit it only took 1m 13s for the Lean component of the CI, which is now only a very small fraction of the full CI) - it seems that there is a lot of useful caching going on...

[Mario Carneiro]

of course, in this situation where you want both anyway, it's better not to do the infinite one

[Mario Carneiro]

although that does make me sad since it's a nice human proof

[Mario Carneiro]

which we are replacing with something that seems not to have a great human explanation

[Terence Tao]

It's still in the blueprint and in the Lean directories, just no longer imported into the optimized final theorem.

[Mario Carneiro]

maybe there should be another entrypoint for the "bonus slides"

[Mario Carneiro]

you probably don't want to have lean code which is not typechecked, it can rot if you aren't validating it periodically

[Terence Tao]

Hmm. Fair point. Not sure what the best solution is here. We could indeed have a ExtraStuff.lean type file that imports all the extra stuff (there are some other side results that could be moved into an extras folder) and have a separate CI check for that (maybe run less often than the main CI).

[Mario Carneiro]

my suggestion is to just have ExtraStuff and check both in CI. I doubt it will be a statistically significant fraction of total CI time

[Mario Carneiro]

you can revisit if something heavy ends up in ExtraStuff

[Mario Carneiro]

but it's probably not worth the CI complexity right now

[Vlad Tsyrklevich]

Based on setting a higher maxHeartbeats, the worst offenders are equational_theories/Generated/Greedy/*, equational_theories/ManuallyProved/Equation1701.lean and equational_theories/Obelix.lean. The latter two are proofs without finite counterexamples, perhaps there are Greedy examples that are not? Those are auto-generated and there are multiple of them, so it seems less sad to remove one or a few of them.

[Mario Carneiro]

My guess is that the autogenerated stuff is actually a CI win to remove in favor of the finite counterexample

[Mario Carneiro]

those translated vampire proofs are surprisingly slow to check

[Terence Tao]

An alternative is to not move or comment out anything (in particular restoring the import Equation854.lean) but once we complete the formalization of both graphs, work on creating a Final.lean file that only imports what is minimally needed to prove the final theorem.

[Vlad Tsyrklevich]

Among the greedy proofs, the only ones I see that immediately stand out that I know have a finite counerexample is 1112=>1629, and 677=>255 is still unknown. So not much to gain there.

[Terence Tao]

My most recent PR did show that commenting out Equation854.lean did not affect the final implication graph. But I'm now leaning towards restoring it so that it stays checked by Lean, even if this adds a few seconds back to the CI.

[Douglas McNeil]

Looking in from the outside, commenting out parts of the code which validate important parts of the paper seems like a misstep unless it's a major win for some tactical or strategic reason. I mean, nobody's actually interested in a random collection of integers.

[Terence Tao]

To be fair, we have millions of (anti-)implications that are coming from such random sets of integers already, the manually proven ones are actually just a tiny fraction of the full graph.

[Terence Tao]

OK. I think what I'll do is restore the import, but add a comment to ManuallyProven.lean that the import is technically redundant for the purposes of establishing the implication graphs.

[Pace Nielsen]

Running

fof(eq1518, axiom, X = mul(mul(Y, Y), mul(X, mul(Y, X)))).
fof(leftcanc, axiom, mul(X, Y) = mul(X, Z) => Y = Z).
fof(leftmultsurj, axiom, ( ! [Y, Z] : ( ? [X] : (mul(Y, X) = Z) ) )).
fof(squaringsurj, axiom, (! [X] : ( ? [Y] : (mul(Y, Y) = X)))).
fof(squaring, axiom, s(X) = mul(X, X)).
fof(sixthpower, axiom, X = s(s(s(s(s(s(X))))))).
fof(squaringhom, axiom, s(mul(X, Y)) = mul(s(X), s(Y))).
fof(extrahom, axiom, f(mul(X, Y)) = mul(f(X), f(Y))).
fof(submagma, axiom, (? [X] : ( X = mul(X, mul(X, mul(X, X))) &  (! [Y] : (f(Y) = X | f(Y) = mul(X, X) | f(Y) = mul(X,mul(X, X)))) ))).
fof(eq47, conjecture, X = mul(X, mul(X, mul(X, X)))).

in Vampire for 999s timed out.

[Douglas McNeil]

I'd say in those cases we're only caring about the _results_, even if there might be interesting stuff lurking there in the same way that MB and BLF have been analyzing 1486 that we just didn't have time to look at more closely. The infinite 854 technology is much more interesting, so it should stay in the validation circle.

Reminds me of ZAK's argument about the risks of automating too early. It's basically an accident that we didn't hit more finite 854 refutations earlier, and then the only thing that we might have thought strange about 854 is that the smallest counterexamples we found were unusually large. Maybe that would've sparked the study of the free magma that actually happened, but maybe not..

[Terence Tao]

Good points. I'll make a note of mentioning this in the (currently unwritten) conclusions portion of the paper.

[Terence Tao]

@Ibrahim Tencer For future reference, here is how one can find the equation number for $x < Sx$:

PS C:\Users\teort\Dropbox\Lean\equational_theories\scripts> py find_equation_id.py "x*(x*x)=(x*x)*(x*x)"
The equation 'x*(x*x)=(x*x)*(x*x)' is Equation 55561: x ◇ (x ◇ x) = (x ◇ x) ◇ (x ◇ x)

[Pace Nielsen]

In line with what @Ibrahim Tencer and @Matthew Bolan have shown, Vampire proves that all 4 open implications involving 1518 are individually equivalent to each other, as well as to getting $S^3=1$, subject to left cancellation. So, in particular, they all equivalent to each other for finite models. Vampire also verifies two implicit facts that come from an earlier computation of @Terence Tao namely that surjectivity of the squaring map yields surjectivity of left multiplication, and that left cancellation implies injectivity of the squaring map.

[Douglas McNeil]

Am I reading right? Does that settle all the 1518s, meaning unless there's a bug in some unformalized argument, 677-255 is the final boss?

[Pace Nielsen]

No, what it does is say that that there are (up to equivalence) just two bosses left.

[Douglas McNeil]

Ah, got you.

[Matthew Bolan]

@Ibrahim Tencer Vampire being able to check the elevation law holds in models of size less than 37 is shocking to me, and I'm having trouble replicating it. Do you mean all models or just ones of the types you list? What settings/TPTP did you run with?

[Terence Tao]

Have we ruled out translation-invariant models for 1518 yet? I am getting hints that there may be a translation-invariant counterexample on ${\mathbf Z}/6{\mathbf Z} \times G$ for some finite abelian group $G$ (in which the squaring map takes the form $S(a,b) = (a+1,b)$, so $S^3 \neq 1$ but $S^6=1$. Note that squaring is automatically a homomorphism in these models, and I also expecting a homomorphism $(a,b) \mapsto (a \hbox{ mod } 3)$ to the cyclic shift with these models.

[Pace Nielsen]

Putting 1518 with left cancellativity, and $S^6=1$ with $S$ a homomorphism, Vampire times out when trying to refute a translation-invariant approach. So you are good to keep trying this avenue!

[Pace Nielsen]

If the cyclic shift example is a submagma, Vampire finds problems with a pure translation-invariant approach. Your proposed examples don't have that issue.

[Pace Nielsen]

(deleted)

[Ibrahim Tencer]

Matthew Bolan said:

Ibrahim Tencer Vampire being able to check the elevation law holds in models of size less than 37 is shocking to me, and I'm having trouble replicating it. Do you mean all models or just ones of the types you list? What settings/TPTP did you run with?

Hmm, I've been reusing the same TPTP file so I would have to go back and check. I probably excluded linear models, possibly the preservation-piecewise models too. It's possible that I included something that I shouldn't have.

@Terence Tao I'm not sure this can work. If squaring is a homomorphism and $S^n = 1$ then we can quotient out by the equivalence generated by $x \sim S^k x$ for some specific $k$. So for each divisor d of n this will give a model where $S^d = 1$. But, it's not too hard to show that if $S^2x = x$ then actually $Sx = x$, so 6 couldn't have been the order of S in the original model. This suggests trying S with order 9 or at least some odd order.

[Terence Tao]

I dont see why $S^6=1$ would force $S^2 x = x$ for any x

[Ibrahim Tencer]

Hmm never mind, that way of quotienting doesn't really make sense.

[Ben Gunby-Mann]

Pace Nielsen said:

I don't know if this is helpful or not, but working with Equation 677, the solutions over a generic field to a linear model $x\diamond y=\alpha x + \beta y$ come in two flavors. Type 1: $\beta$ is a primitive 5th root of unity (i.e. a root of $x^4+x^3+x^2+x+1$) and $\alpha=1-\beta$. Type 2: $\beta$ is a root of $x^4+x^3+2x^2+2x+1$ and $\alpha=-\beta^3-\beta-1$.

Possibly worth noting is that in the Type 2 solutions, $\alpha$ is a primitive cube root of unity (as when $y=-x^3-x-1$, we have $x^4+x^3+2x^2+2x+1|y^2+y+1$). (Furthermore but less interestingly, if $\alpha=\omega$ is a primitive cube root of unity, then $\beta$ satisfies the quadratic $\beta^2-\omega\beta-\omega=0$; this gives the two solutions for each possible $\alpha$.)

Interestingly, any linear model with $\alpha$ a primitive cube root of unity satisfies 255, regardless of $\beta$. (The necessary equation factors as $(\alpha^2+\alpha+1)(\alpha+\beta-1)=0$.)

[Terence Tao]

I'm now thinking that a variant of the 503 construction should be able to refute the 1518 implications, though the example may end up being rather large (larger than the 84-element 503 example).

The equation 1518 is $L_{Sy} L_x L_y x = x$. Replacing $x$ by $L_{Sy} x$ and then cancelling $L_{Sy}$, one can rewrite this equation as $(L_{Sy} x) \cdot (L_y L_{Sy} x) = x$. If we use $x \stackrel{y}{\to} z$ to denote the relation $L_y x = z$ (think of this as "labeling" the directed edge $x \to z$ by $y$, we can interpret this law as follows: given a labeled 2-path of the form
$x \stackrel{Sy}{\to} z \stackrel{y}{\to} w$
we have $z \cdot w = x$, or equivalently $w \stackrel{z}{\to} x$. To put it another way, if we define a good cycle to be a cycle
$x_0 \to x_1 \to x_2 \to \dots \to x_{n-1} \to x_0$
in the magma with the property that $x_{i-1} = x_i \cdot x_{i+1}$ for all $i$ (extending indices periodically by $n$), then (by the bijectivity of left multiplication and finiteness) every directed edge extends uniquely to a good cycle, and if the edge $x_0 \to x_1$ can be labeled by $y$, then the edge $x_{n-1} \to x_0$ must be labeled by $Sy$ (in fact this is an if and only if), and the rest of the cycle also can be similarly labeled as
$x_0 \stackrel{y}{\to} x_1 \stackrel{S^{n-1} y}{\to} x_2 \stackrel{S^{n-2} y}{\to} \dots \stackrel{S^2 y}{\to} x_{n-1} \stackrel{Sy}{\to} x_0.$
If we do not have $S^n y = y$, then we can keep iterating and get more labels. For instance, if we had $n=3$ and $S^6 y = y$, then the label
$x \stackrel{y}{\to} z \to w \to x$
on the first edge of the good cycle $x \to z \to w \to x$ iterates to
$x \stackrel{y, S^3 y}{\to} z \stackrel{Sy, S^4 y}{\to} w \stackrel{S^2 y, S^5 y}{\to} x.$

So one can hope to build a 1518 magma by first designating some cycles in the magma as "good cycles", and then trying to label the edges of these good cycles with elements $y$ of the graph consistent with the above law (as well as the fact that given a good cycle $x_0 \to x_1 \to \dots \to x_{n-1} \to x_0$, one must have $x_{i+1} \stackrel{x_i}{\to} x_{i-1}$ as part of another good cycle), in order to generate the full multiplication table.

At first glance this looks like a terrible strategy, because we need every vertex $x$ to have exactly one outgoing edge $x \stackrel{y}{\to} z$ for a given $y$, and this looks like a very severe constraint. However, if the magma has a lot of idempotents, then the task is much easier, due to the following observation. Suppose that one has a partially defined magma operation $\diamond$ such that $y \diamond y = Sy$ is always defined, and that $y \diamond x$ is defined if $x$ or $y$ are not idempotent ($Sx \neq x$ or $Sy \neq y$); so we permit $y \diamond x$ to be undefined when $x$, $y$ are both idempotent. We also impose left-injectivity, as well as the partial 1518 law that if $L_{Sy} x$ is defined, then $(L_{Sy} x) \diamond (L_y L_{Sy} x)$ is defined and equal to $x$ (in terms of graphs, this means that if we have $x \stackrel{Sy}{\to} z \to w$ where $x \to z \to w$ is part of a good cycle in the sense that $z \diamond w = x$, then we can propagate the label to $x \stackrel{Sy}{\to} z \stackrel{y}{\to} w$). Then we can complete the partial 1518 operation to a complete 1518 operation by setting $y \diamond x = x$ whenever $y \diamond x$ was undefined (in @Ibrahim Tencer's notation, we force the elevation relation $y < x$).

The upshot of this is that if we find a partial 1518 operation that is total for non-idempotents, we can extend the table to the idempotents as well. So one just needs enough good cycles and labels on the good cycles to cover the non-idempotents while respecting axioms such as left-injectivity, and then we can solve the problem. With some pen and paper I think I found a seed involving twelve non-idempotents, generated by two generators $0, 0'$ of order $6$ in the sense that $S^6 0 = 0$ and $S^6 0' = 0'$; writing $i = S^i 0$ and $i' = S^i 0'$, the initial seed takes the form of good cycles
$a_i \stackrel{i+1,i+2}{\to} i \stackrel{i,i+1}{\to} i+1 \stackrel{i-1,i}{\to} a_i \stackrel{i-2,i-1}{\to} i' \stackrel{i-3,i-2}{\to} (i+1)' \stackrel{i-4,i-3}{\to} a_i$
for $i=0,\dots,5$ and some idempotents $a_0,\dots,a_5$. One has to keep extending this seed with additional cycles to maintain all the required laws, for instance $i' \stackrel{a_i}{\to} i+1$ needs to be extended to a good cycle, but I think I can do this by a sort of greedy algorithm (adding fresh idempotents whenever needed) that terminates in finite time. It got too hard to do this with pen and paper though. I may try to write this strategy more formally in a blueprint chapter later today.

[Matthew Bolan]

I think I can program this up for you if needed.

[Terence Tao]

OK, I will try to write up more detailed notes later today to share on this, and hopefully they will be enough to set up some variant of a seed-finding algorithm.

[Matthew Bolan]

Possible that I've typoed something, but I think my existing tools are already telling me that

============
1 2 3 4 5 1
1 1 0 2 _ _
3 4 2 _ 0 _
4 5 _ 3 _ 0
1 _ 0 2 4 _
1 _ 0 2 _ 5
============

is a partial 1518 operation that is total for non-idempotents and violates 47 (In this case the only non-idempotent is 0). I guess I'll try and implement the extension procedure and see if this breaks somehow.

[Terence Tao]

Hmm, this will have to break somehow because squaring is necessarily a bijection on 1518 magmas, but it will be instructive to see where the breakage is actually happening.

[Matthew Bolan]

I imposed that if $x \diamond (y \diamond x)$ and $y \diamond y$ are defined, then $x = (y \diamond y ) \diamond (x \diamond (y \diamond x))$, should I have imposed some stronger form of 1518? I also can impose auxiliary laws as for any other seed, perhaps squaring being a bijection is an obvious one to include.

[Matthew Bolan]

Actually, I think I may have typoed something, one moment.

[Matthew Bolan]

No, it seems fine. Some testing code didn't run, but the testing code still says the table is fine.

[Terence Tao]

I think the laws needed are (a) $Sy = y \diamond y$ is always defined and is a bijection; (b) If $y \diamond x$ is undefined, then $y,x$ are both idempotents; (c) If $y \diamond x = y \diamond z$ then $x=z$; (d) If $Sy \diamond x$ is defined then $(Sy \diamond x) \diamond (y \diamond (Sy \diamond x))$ is defined and equal to $x$ (this is a rearrangement of of 1518). I'm writing up notes now, but it may take an hour or so before I am done, so take the above rules with a grain of salt before then.

[Terence Tao]

Ugh, there are significant technical difficulties in my entire approach - making most of the magma idempotents actually seems to create a lot of inconsistencies that don't seem easy to fix. Best to just ignore my previous proposal for now.

[Matthew Bolan]

I've cleaned up my cohomology script and in particular can allow linear models on general finite fields for $M$ now. No real new results to report, except that the order of the 1110 counterexample can be reduced from 25 to 16 (as Terry already anticipated). I had a mistake in the code for specifically this reduction - this order 16 model is only a counterexample to 4435 and not 1629. For 1629 we still need to use the original order 25 example.

[Matthew Bolan]

1516 -> 1489 counterexample can be reduced from size 49 to size 35

[Douglas McNeil]

That's below the limit Vlad guessed would be fine without heartbeat changes!

[Matthew Bolan]

The counterexample to 1076 -> 2294, 4435 can be reduced from order 169 to 65, but that's not small enough to link in zulip.

[Matthew Bolan]

1076_order_65.txt

[Matthew Bolan]

I can get the counterexample to 503 -> 4065, 3862 down from 50 to 45

[Matthew Bolan]

503_order_45.txt

[Matthew Bolan]

45 might still be too large, but if someone formalizes the cohomology method this provides an avenue to resolving https://github.com/teorth/equational_theories/issues/953

[Terence Tao]

What procedure did you use to shrink the 503 example?

[Matthew Bolan]

That's just the cohomology construction, unrelated to your original example.

[Matthew Bolan]

Code says

G is (0)x+(2)y in Finite Field of size 5, M is (z2 + 1)x+(2*z2)y in Finite Field in z2 of size 3^2.

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

Wow!

I must say, in hindsight I'm glad I spent a bit of extra time on optimizing the FME back in October, these are much larger than anything I expected to ever show up.

[Matthew Bolan]

Those were the result of trying $M,G$ linear magmas on finite fields. I might now try to choose some select non-linear models for 1076 (and maybe 503) to try and get that 65 down a little more.

[Matthew Bolan]

I'd quite like to allow $M$ to be any finite abelian group, but I feel like this won't gain too much and in order to do it I need to change how the linear algebra is currently done.

[Terence Tao]

I think if $M$ is the direct product of two factor magmas $M_1,M_2$, then in order for the cohomological construction to produce a counterexample for $M$, it must have already done so for one of the two components $M_1, M_2$ (otherwise the cocycle equation for the consequent would be obeyed for both components of the cocycle, and hence for the full cocycle). In practice I think this means the finite field choices for $M$ already suffice.

[Matthew Bolan]

I agree, but $M$ being the integers modulo a prime power could maybe offer something, and the fact $M$ is a direct product of abelian groups doesn't mean its a direct product of factor magmas (finite fields are already an example of this).

[Terence Tao]

Ah, right, we have some "non-semisimple" linear models as well. Yes, in principle these could give some new constructions.

[Terence Tao]

Though I think a model formed by a ${\mathbf Z}/4{\mathbf Z}$-extension, say, could also be viewed as a tower of two ${\mathbb F}_2$-extensions. The first extension might not necessarily produce a direct counterexample, but could make a sufficiently novel and interesting new magma that when plugged in to the cohomology machine as a new base model, it can create a counterexample upon applying a second extension. So if your software can detect the existence of non-trivial extensions by finite fields (ones where the extension isn't a coboundary), these might be useful base models for a second extension which may capture at least some of the cyclic group of prime power order examples.

[Terence Tao]

It's hard to imagine getting a magma of order <45 out of this though, at least if we don't have a useful ${\mathbf F}_2$ linear model to play with

[Matthew Bolan]

That makes sense, after all $\mathbb Z/4\mathbb Z$ is a central extension of $\mathbb Z/2\mathbb Z$. Currently my code just computes $Z^2$ for both laws, but I can definitely compute the actual $H^2$ without much trouble.

[Terence Tao]

In analogy with the Schur-Zassenhaus theorem, I expect the cohomology $H^2$ to be trivial when $G$ and $M$ are "unrelated" (in the group theory setting, this means that $G$ and $M$ have coprime order, but I don't know if that's the right condition in the magma setting). So it's interesting that you got an order 65 example and an order 45 example, it suggests that a naive version of Schur-Zassenhaus is not true for magmas.

[Terence Tao]

Maybe that's not so surprising. Most of group theory is also not true for magmas.

[Matthew Bolan]

I also noticed that $M$ didn't change between my original models for 1516 and 1076 and these new ones.

[Matthew Bolan]

Hmm, actually that's a little wrong for the 1516 examples I shared. The 1516 example switched from $4x+5y \pmod 7$ to $4x+y \pmod 7$ for $M$ (though had I copy pasted slightly different options $M$ would have stayed the same). There are also examples for 1516 without a magma modulo 7 for $M$, such as one of order 45 where

G is (1)x+(2*z2)y in Finite Field in z2 of size 3^2, M is (3)x+(3)y in Finite Field of size 5.

[Matthew Bolan]

A bit of a silly question, but does 1076 even have any known small (order < 13) non-linear models?

[Matthew Bolan]

Hah, turns out that if you restrict to the submagma generated by the counterexample, the 503 counterexample becomes only order 36. I think this means that I could have taken $G$ to be an order $4$ submagma of the linear order $5$ magma my program found.

[Matthew Bolan]

This is for its twin 476 and not 503, but that shouldn't make a difference

[Matthew Bolan]

And here it is for 503

[Matthew Bolan]

For the others the counterexample (at least the one found by FME) generates the entire magma. I also discovered that my reduction of the original 1110 counterexample from order 25 to 16 was incorrect - somewhere along the way I accidentally switched the law it was supposed to be falsifying from 1629 to 4435.

[Matthew Bolan]

1076 just doesn't seem to have many small models (I have found no nonlinear ones so far, Mace 4 is currently checking order 9), so it is going to be very hard to improve on the order 65 counterexample to 1076 -> 2294, 4435 with current ideas.

[Amir Livne Bar-on]

Is there a listing of the full parameters of counter-examples found this way? Maybe there are additional conditions they happen to satisfy? (Especially if these conditions limit the space of endomorphisms to consider)

[Matthew Bolan]

For the most part, it's the ones I've shared here. I think there were a few others, but for the most part I've been stopping runs once the first example is found.

[Amir Livne Bar-on]

Oh, so the coefficients given for G are the M endomorphisms from the blueprint?

[Vlad Tsyrklevich]

@Matthew Bolan Have you tried seeing if Lean accepts these? I'm not sure if you have a working dev environment, I can test it for you if you like, but obviously feel free to test it yourself.

[Matthew Bolan]

I have not tried. While I do have a working dev environment, I have no experience with lean so it is probably better for someone else to do it. The order 65 example is still pretty large, and probably won't get much smaller, so if we wish to formalize it we're going to have to formalize enough of the cohomology stuff anyway. Despite the fancy language, I don't think that should be too difficult. There is also a possibility that future examples will be massive, or that the idea is applied to some of the unformalized infinite implications.

[Matthew Bolan]

Amir Livne Bar-on said:

Oh, so the coefficients given for G are the M endomorphisms from the blueprint?

The coefficients of $M$ are the endomorphisms from the blueprint. I currently restrict myself to those endomorphisms coming from multiplication in the underlying field.

[Vlad Tsyrklevich]

Matthew Bolan said:

While I do have a working dev environment, I have no experience with lean so it is probably better for someone else to do it.

I would just do to do the same thing as you would anyway: add them to All4x4Tables and run lake build to see if it builds successfully or not.

[Terence Tao]

I found a massive (N = 522) counterexample to all the 1518 refutations. FME refuses to provide a URL but still (grudgingly) accepts the text input:
output.txt

And here is the python code needed to generate that file:
array.py

My previous approach of building good cycles and dissipating all the consequences of 1518 into idempotents did eventually work, but was significantly more complicated than expected, and due to the need to keep a lot of the cycles disjoint from each other, I needed a lot of "space", leading to the large value of N.

While this approach technically works, it may be too complex to verify in Lean. (The counterexample does have a symmetry of order 12, so one can reduce the verification time a little bit from O(522^2) to O(522^2/12) in principle, but this is still unappetizing.) It may be good to find an alternate approach.

[Terence Tao]

The basic strategy was to use the following interpretation of 1518, writing $x \stackrel{y}{\to} z$ for $y \diamond x = z$: every "good cycle" of the form $\dots x_{-1} \stackrel{Sy}{\to} x_0 \stackrel{y}{\to} x_1 \dots$ will generate further edges $x_1 \stackrel{x_0}{\to} x_{-1}$, $x_2 \stackrel{x_1}{\to} x_{0}$, etc., which must themselves be placed in good cycles. This process could iterate indefinitely, but if one has some idempotents $x,y$ which are right-absorptive with respect to each other in the sense that $x \diamond y = y$ and $y \diamond x = x$, then any good 2-cycle of the form $x \stackrel{z}{\to} y \stackrel{z}{\to} x$ where $z$ is also idempotent, will iterate to the 1-cycles $x \stackrel{y}{\to} x$, $y \stackrel{x}{\to} y$, which then iterate to the idempotent 1-cycles $x \stackrel{x}{\to} x$, $y \stackrel{y}{\to} y$ which are self-consistent (no further good cycles generated). So it is "just" a matter of starting with a good cycle that captures a counterexample to the desired law and iterating it (placing new good cycles in locations that do not cause collisions, and re-using good cycles whenever possible to avoid a combinatorial explosion) until all the non-idempotents are gone and the cycle can be iterated to the 2-cycles of the above form. This however took longer than expected; the magma contains 12 non-idempotents (which basically hold the counterexample) but also 510 idempotents (to hold all the iterations arising from the counterexample).

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

Terence Tao said:

I found a massive (N = 522) counterexample to all the 1518 refutations. FME refuses to provide a URL but still (grudgingly) accepts the text input

Great work!

The maximum length of a valid URL is technically 2048 ascii characters, so there's no way to fit this example without implementing some kind of compression :sweat_smile:

If another approach turns out to be difficult, I think it'd be possible to verify this in-kernel using some technical tricks (e.g. divide-and-conquer, split into separate proofs which are smaller and together imply the result, should not be too hard) or by formalizing the construction and some kind of ceritifcate that the construction terminates successfully which is smaller than the entire optable (might be hard).

[Alex Meiburg]

In terms of evaluating that effectively: the table is still mostly the right-absorptive law. If the number of exceptions was O(1), then docs#Function.update - or equivalently, writing it like f x y : = if (x = 7 ∧ y = 13) then 7 else y - could be a more efficient representation, and most of the verification could be done "analytically".

But in this case, ~17% of the grid is not right-absorptive, which is a pretty sizable fraction. But if there's a clean representation of most of the exceptions, that could definitely help.

Have you checked if the magma has any nontrivial quotients that still witness the desired nonimplication?

[Terence Tao]

I have not attempted any compression. It was possible to compress the (somewhat similar) 503 construction from size 84 to size 50, and I would imagine a similar compression would be possible here, though doing so destroys the symmetries and so may not actually be a net win.

There is a lot of flexibility in the construction and it may be possible to get the size down to something more like 100 with more clever choices, though that's still rather large.

One can phrase 1518 in the following form: if a triple $(a,b,c)$ is of the form $(x, Sy \diamond x, y \diamond (Sy \diamond x))$, then $b \diamond c = a$. Ordinarily this would take $O(N^2)$ verifications, but for this magma the number of triples $(a,b,c)$ is a lot smaller than $N^2$ because it is designed to have a lot of repetition. For instance, due to the mostly right-absorptive nature, most of the triples end up being just $(a,a,a)$. A back of the envelope calculation suggests that the number of triples is of the order of 1000, and after reducing by symmetries there are actually about 100 or so. So there may be a way to implicitly describe the multiplication operation that makes it easier to certify. (The triples are the length two subpaths of the "good cycles", of which there are about 170 or so of length 6, another 100 or so of length 2, and the rest are loops of length 1 or of a very simple form.)

[Vlad Tsyrklevich]

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

The maximum length of a valid URL is technically 2048 ascii characters, so there's no way to fit this example without implementing some kind of compression :sweat_smile:

We should all be using the fragment identifier (#) instead of the query string (?), the query string is (needlessly) sent to the server and causes poor cache behavior, the fragment identifier is local to the browser and has a much larger size limit. (Graphiti also uses the query string and shouldn't to accept larger inputs)

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

@Vlad Tsyrklevich Agreed. I originally did it this way to take advantage of Elm's query string key-value parser, but the features this gave me for free ended up being unused, and the current version bypasses the key-value parsing anyway. I plan to update it to support # eventually, but now it'll have to support both (not doing so would break existing URLs).

[Vlad Tsyrklevich]

Yeah, I've meant to do the same but it's just lost in the other list of TODOs

[Kevin Buzzard]

I have a completely dumb question. Everyone seems to be happy with the idea "obviously 522^2 is too big for Lean" but if you take a step back and ask the question "is 522^2 too big for a computer program" the answer is clearly "no, it's no longer the 1950s". I remember writing code in Lean 3 about checking some equality in 3 variables mod 3 and discovering that doing the brute force approach of checking all 27 cases was surprisingly slow; I learnt from that that 27 was a big number for Lean 3 to count up to, but everyone assured me that Lean 4 was on the way, and Lean 4 was a proper programming language, not just a research project, and that Lean 4 was as fast as Haskell in some test cases. So what is actually going on here?

Here's a concrete question: can one use this funny extra reduceBool axiom to actually do this 522 calculation? And another one: can one do the calculation without the extra axiom? Or do we really have to come to terms with the fact that 522^2 is not a number that Lean can count up to? There's a program in Coq which worked out and formally verified the first million digits of pi. I bet 522^2 isn't too big for Coq.

[Vlad Tsyrklevich]

I think someone that knows Lean internals better would have to say why Lean chokes on such small operation tables, it may be that we're just using the system poorly.

[Bruno Le Floch]

Even just def matrix : Array (Array Nat) := #[#[1,2],#[3,4]] takes forever for a 522 times 522 matrix. I tried with UInt16 or UInt32 instead of Nat with no success. ChatGPT suggests using a ByteArray and reimplementing whatever operations we need, in particular indexing ourselves in the ByteArray. This is a bit annoying because the entries of the multiplication table are bigger than a Byte so we have to work with pairs of Bytes. It seems doable though, and (almost) certain to use a flat storage, rather than nested pointers all over the place.

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

Bruno Le Floch said:

Even just def matrix : Array (Array Nat) := #[#[1,2],#[3,4]] takes forever for a 522 times 522 matrix.

What happens if you create an Array (Array Nat) of the same dimension programmatically by using a short program to fill in the entries, say (x,y) \mapsto x, instead of giving an explicit definition in the source? Does it still choke? I'd test this myself but don't have a working Lean4 installation at the moment.

[Bernhard Reinke]

Kevin Buzzard said:

I have a completely dumb question. Everyone seems to be happy with the idea "obviously 522^2 is too big for Lean" but if you take a step back and ask the question "is 522^2 too big for a computer program" the answer is clearly "no, it's no longer the 1950s". I remember writing code in Lean 3 about checking some equality in 3 variables mod 3 and discovering that doing the brute force approach of checking all 27 cases was surprisingly slow; I learnt from that that 27 was a big number for Lean 3 to count up to, but everyone assured me that Lean 4 was on the way, and Lean 4 was a proper programming language, not just a research project, and that Lean 4 was as fast as Haskell in some test cases. So what is actually going on here?

Here's a concrete question: can one use this funny extra reduceBool axiom to actually do this 522 calculation? And another one: can one do the calculation without the extra axiom? Or do we really have to come to terms with the fact that 522^2 is not a number that Lean can count up to? There's a program in Coq which worked out and formally verified the first million digits of pi. I bet 522^2 isn't too big for Coq.

I glanced at the conclusion of the linked paper; it seems to me that they need to trust native_compute, so also a compiler.

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

Kevin Buzzard said:

I remember writing code in Lean 3 about checking some equality in 3 variables mod 3 and discovering that doing the brute force approach of checking all 27 cases was surprisingly slow

My infinite model showing Equation1701_not_implies_Equation4587 requires a similar (but 120-fold) case distinction, and it's really quite slow. I asked if people knew any techniques to improve it, but none of the suggestions resulted in major performance gains.

I bet 522^2 isn't too big for Coq.

From experience, as someone who worked on some very big proofs, 522^2 can be too big for most proof assistants in certain similar circumstances, including Coq, and even proof assistants based on very different formalisms such as Isabelle/HOL. And while 522^2 is trivial in terms of pure computational verification (the Finite Magma Explorer completes the check above in a fraction of a second; a C program would be much faster still), it's just about at the threshold where I'd not be surprised if it started being substantial work in terms of "creating and storing a more complicated proof object".

[Bruno Le Floch]

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

What happens if you create an Array (Array Nat) of the same dimension programmatically by using a short program to fill in the entries, say (x,y) \mapsto x, instead of giving an explicit definition in the source? Does it still choke? I'd test this myself but don't have a working Lean4 installation at the moment.

Sorry, I'm struggling with the Lean syntax so I wasn't able to test that easily. I will try tonight.

[Amir Livne Bar-on]

Just checked, it's immediate to create an array of any size. But if you try to index a large array like arr[4][2] you get "maximum recursion depth has been reached" when calculating or verifying a theorem that depends on the value. This error also comes very quickly.

[Shreyas Srinivas]

that's easy

[Shreyas Srinivas]

When you do indexing like that the proof of correctness is constructed by omega

[Shreyas Srinivas]

If instead you use unsafe indexing it works fine.

[Shreyas Srinivas]

See below:

def ex : Array <| Array Nat := mkArray 1122 (mkArray 512 12)

#eval ex[134]![123]! -- works. no proofs. panic if index out of bounds

#eval ex[134][123]  -- max recursion

[Shreyas Srinivas]

For proofs, I have to guess lean is using the unary Nat representation

[Shreyas Srinivas]

The following also works:

def ex : Array <| Array Nat := mkArray 1122 (mkArray 512 12)

#eval ex[134]![123]! -- works

set_option maxRecDepth 10000
#eval ex[134][123]  -- no more max recursion error. Now it works

[Shreyas Srinivas]

And for what it is worth, 522^2 is definitely not too big for lean:

#eval 522^2
#reduce 522^2
example : 522^2 = 272484 := by rfl

[Shreyas Srinivas]

The comparison with haskell is not fair because haskell does no static checking of index bounds whatsoever

[Mario Carneiro]

Shreyas Srinivas said:

For proofs, I have to guess lean is using the unary Nat representation

no

[Mario Carneiro]

Kevin Buzzard said:

I have a completely dumb question. Everyone seems to be happy with the idea "obviously 522^2 is too big for Lean" but if you take a step back and ask the question "is 522^2 too big for a computer program" the answer is clearly "no, it's no longer the 1950s".

I encourage you to keep this attitude. Our proof assistants are too slow by orders of magnitude and we need people to push for better

[Mario Carneiro]

In any case, I think this is an interesting challenge to do via the kernel and straightforwardly doable using native_decide

[Shreyas Srinivas]

Btw, here's a more fancy example which easily does the first eval but gets stuck on the second eval:

import Mathlib

def ex : Array <| Array Nat := @Array.ofFn (Array Nat) 512 (fun i => @Array.ofFn Nat 512 (fun j => i + j))

set_option maxHeartbeats 1000000
set_option maxRecDepth 10000

#eval ex[134]! -- works. no proofs. panic if index out of bounds

#eval ex[134]  -- stuck for a long time before giving answer

[Daniel Weber]

The main problem with using the kernel is the inefficiency of random access, right? I wonder how efficiently we can do the verification of the table as a circuit, that might be a good model

[Mario Carneiro]

The fact that this is compressible to a small python file tells me that the proof is for sure smaller than 512^2 verifications anyway

[Mario Carneiro]

It would be interesting to verify the computation directly but IMO that would destroy a lot of structure

[Bruno Le Floch]

I'm having a bit of success manipulating very large ByteArray quickly, indexing them, etc. The main difficulty is to create them since the typical techniques go through an Array or List, which is too slow. Instead, I load a binary file that stores the entries of the multiplication table as pairs of bytes. Do we want to pursue that direction? It seems quite ugly to have the proof depend on a binary data file, and it will necessitate a bit of work to prove that the calculations on packed ByteArray really check the magma equations.

[Terence Tao]

OK, I think I am beginning to understand the issue with verifying the order 522 example efficiently in Lean. As pointed out previously, it mostly has to do with the lack of support in Lean for efficient random access memory.

Roughly speaking, the operation $\diamond$ on the order 522 example is defined by $N$ parametric rules for $N \approx 20$, with each rule taking the form

• Rule $j$: For all $i \in A^{(j)}$, we have $x^{(j)}_i \diamond y^{(j)}_i = z^{(j)}_i$.

Here $A^{(j)}$ is some explicit set and the functions $i \mapsto x^{(j)}_i$, $i \mapsto y^{(j)}_i$, $i \mapsto z^{(j)}_i$ are all very simple and decidable. Here is a simplified example rule:

• Sample rule: For all $i \in \mathrm{Fin}\ 6$, $j \in \mathrm{Fin}\ 6$, $s = \pm 1$, we have $(-1,j,s,i) \diamond (0,6,s,i) = (1,j,s,i)$.

(Actually, to get to $N \approx 20$ rules instead of like $N \approx 200$, one has to add extra parameters here, but this should convey the general idea.)

Furthermore - and this is the tricky thing - there is a default rule:

• Default rule: If $x \diamond y$ is not defined by any of the previous rules, then $x \diamond y = y$.

In order to verify that this creates a counterexample, one first has to verify that the rules don't collide with each other, so for two different rules, Rule $j$ and Rule $j'$, one has to verify that the $(x^{(j)}_i, y^{(j)}_i)$ are distinct from the $(x^{(j')}_{i'}, y^{(j')}_{i'})$. This is tedious but with $N \approx 20$ or so rules I can imagine these $O(N^2)$ case checks are within the capability of Lean.

The harder thing is that there are going to be about $N^2$ claims of the sort "For all $i$ in some set $A$, the operation $x_i \diamond y_i$ is covered by the default rule and is thus equal to $y_i$". To verify this, we need to show that $x_i \diamond y_i$ is not covered by each of the $N$ other rules, and so this leads to $O(N^3)$ case checks, which makes the complexity on par with the brute force $O(522^2)$ calculation using a random access memory array to store the multiplication table.

In any event, even if we find some ad hoc way to make this particular calculation work, I agree with Kevin that it would be a much more useful contribution in the long term if we figure out how to give Lean the ability to efficiently work with random access arrays.

[Amir Livne Bar-on]

Running the script with J = 5 gives a magma of order 438 that's also a counter-example to the 4 equations

[Amir Livne Bar-on]

How hard would it be to prove that some arbitrary high J would work? It would be nice to formalize this, whether or not we manage to convince Lean to brute-force check this magma

[Amir Livne Bar-on]

(quantitative arguments are always a bit complicated, e.g. so far all the greedy constructions so far use the free group rather than familiar groups)

[Terence Tao]

Hmm, this could be a promising direction. A lot of my design choices for the magma were focused on keeping the magma small, so I kept reusing elements whenever I could, but this led to a lot of potential collisions to avoid. If I stop caring completely about making the magma small, then I can spread out the elements I need much more widely (in a similar spirit to the greedy algorithms) and there should be a lot fewer collisions that need checking. I could potentially run this as basically a greedy algorithm that happens to terminate in finite time. Let me think about this.

[Kyle Miller]

Terence Tao said:

it mostly has to do with the lack of support in Lean for efficient random access memory.

Something that's a bit interesting about kernel typechecking is that there's a lot of caching — so it might actually be that random access of a List can be faster than you think. It's sort of inefficient (keys would look something like List.get! lst 37), but it's random access nonetheless.

Is there a summary somewhere of what it would mean to verify output.txt? If I have time today, I might try taking up the challenge.

[Amir Livne Bar-on]

Equation 1518 is M[M[y][y]][M[x][M[y][x]]] == x (for all x and y).

All counter-examples are at 0, so

M[0][M[0][M[0][0]]] != 0            eq 47
M[0][M[0][M[M[0][0]][0]]] != 0      eq 614
M[0][M[M[0][0]][M[0][0]]] != 0      eq 817
M[M[0][M[0][0]]][0] != M[0][0]      eq 3862

[Daniel Weber]

Here's a potential approach for kernel verification: for every x, y we precompute 3 values — $y\diamond x,Sy, x\diamond (y\diamond x)$. This gives four values of the operation, so we just need to verify that there's at most one value for any input. If we have all of these values in one list, then we can sort it, and then it can be verified in one scan of the array. Can the kernel do (linked-list-friendly) merge sort efficiently enough?

[Alex Meiburg]

Mario Carneiro said:

The fact that this is compressible to a small python file tells me that the proof is for sure smaller than 512^2 verifications anyway

That was my first thought as well, but the Python file doesn't describe a construction that "obviously" (as in, for a reason transparent to a human) works, I think. My understanding is more that it takes an operation table and gradually modifies it to try to make more and more properties desirable. It turns out that after ~40k such modifications (which do mostly have a nice structure), the construction closes.

It's possible there's a clever way to prove (in the normal human sense) that the construction closes, which could then certainly be translated to Lean, but I don't think there was such a proof in mind when the code was written. @Terence Tao can correct me there if I'm wrong. :)

[Terence Tao]

Yeah, I don't yet have a formal proof that this method had to work eventually, but instead it was an iterative process as you describe where the 1518 law was holding on most of the magma but had some places where the law was failing. I could fix that by tweaking the magma operation (and sometimes adding additional elements), but (a) sometimes this caused unwanted collisions with previous rules, requiring me to backtrack and try a different tweak, and (b) the tweak would generally introduce new violations. For (b) there was a strong sense that I could make the new violations be "simpler" than the previous violations, ultimately to the point where I could resolve the violations by enforcing the right absorptive law on the offending elements, but dealing with (a) was an ad hoc process where I would repeatedly implement a proposed solution in python and it would report a collision that I did not expect, forcing me to make the solution more complicated and larger each time. But this was in large part because I was recycling elements quite often to save space, which created a much higher density of potential collision scenarios. Following Amir's suggestion, I am now trying to see if one takes a much more "greedy" approach in which one just keeps introducing new idempotent elements to fix previous violations without any effort to reuse them, then one can close the argument in finite time. (I'm pretty certain that one can create an infinite example this way, and indeed we essentially did this for our main project; the trick is to somehow capture the property (b) I was empirically observing of the violations getting "simpler" as the iteration progressed, even if the number of such violations starts to increase exponentially.)

[Mario Carneiro]

I still think that this process yields a much smaller list of things to check than 512^2. It's structured as a small number of modifications on a large table, and because of that the list of things to check is only approximately the square of the number of modifications rather than the whole table

[Mario Carneiro]

I got distracted earlier but I'm working on a formalization of this (human) definition, but I encourage those playing with the "data dump" approach to continue

[Mario Carneiro]

Amir Livne Bar-on said:

How hard would it be to prove that some arbitrary high J would work? It would be nice to formalize this, whether or not we manage to convince Lean to brute-force check this magma

I expect this version of the proof to be even easier than the J = 5 version, if you can figure out how to structure it

[Kyle Miller]

I've got a proof of M[M[y][y]][M[x][M[y][x]]] == x running, let's see if it completes. I got it to verify for all 0 <= x, y < 50 in 7.7 seconds, so maybe it'll be done in about 15 minutes.

To use this, you take the array itself and put it into a file named data_1518.txt in the same directory.

code

import Mathlib

open Qq
open Lean Elab
open Std.Internal.Parsec
open Std.Internal.Parsec.String

def parseArray {α : Type} (p : Parser α) : Parser (List α) := do
  ws *> skipChar '['
  let arr ← many (ws *> p <* optional (ws *> skipChar ','))
  ws *> skipChar ']'
  return arr.toList

def parseData (data : String) : IO (List (List Nat)) := do
  match parseArray (parseArray digits) (String.mkIterator data) with
  | .success _ v => return v
  | .error _ err => throw <| IO.userError err

elab (name := includeStr) "def_nat_matrix " id:ident str:str : command => Command.liftTermElabM do
  let some str := str.1.isStrLit? | throwUnsupportedSyntax
  let srcPath := System.FilePath.mk (← MonadLog.getFileName)
  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
  let path := srcDir / str
  let data ← IO.FS.readFile path
  let matrix ← parseData data
  addDecl <| .defnDecl {
    name := id.getId
    levelParams := []
    type := q(List (List Nat))
    value := toExpr matrix
    hints := .regular 0 -- avoid unfolding matrix in kernel defeq
    safety := .safe
  }
  Term.addTermInfo' id (mkConst id.getId) (isBinder := true)

def_nat_matrix data_1518 "data_1518.txt"

/-- Ensure the `Nat` is reduced before evaluating `f` -/
def nat_seq {α : Type} (n : Nat) (f : Nat → α) : α :=
  match n with
  | 0 => f 0
  | .succ n => f (.succ n)

def matrix_get (M : List (List Nat)) (i j : Nat) : Nat :=
  nat_seq i (fun i => nat_seq j (fun j => (M.getD i []).getD j 0))

/-
`M[M[y][y]][M[x][M[y][x]]] == x` for all `x` and `y`.
-/
def verify_rule (M : List (List Nat)) : Bool :=
  let n := M.length -- took 7.7 seconds when this was set to 50
  Nat.fold (n := n) (init := true) fun x b => b &&
    Nat.fold (n := n) (init := b) fun y b => b &&
      matrix_get M (matrix_get M y y) (matrix_get M x (matrix_get M y x)) == x

set_option maxRecDepth 5000

elab "kernel_rfl_true" : tactic => Tactic.liftMetaTactic1 fun g => do
  g.assign <| ← Meta.mkExpectedTypeHint (← Meta.mkEqRefl (mkConst ``true)) (← g.getType)
  return none

set_option profiler true
theorem rule_verified : verify_rule data_1518 = true := by kernel_rfl_true

[Kyle Miller]

Oh, hm, I just ran out of RAM and had to kill it.

[Mario Carneiro]

does it work in native_decide?

[Kyle Miller]

Haven't tested, because I'm skipping the compiler when I add the matrix to the environment

[Kyle Miller]

(I haven't had the patience to wait for the compiler to compile this large literal... Is there any way to say "this is already in memory, please use it!"?)

[Kyle Miller]

At least I could try doing what native_decide would do manually. The M[M[y][y]][M[x][M[y][x]]] == x rule holds, according to verify_rule.

def test_verify (filename : String) : TermElabM Bool := do
  let srcPath := System.FilePath.mk (← MonadLog.getFileName)
  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
  let path := srcDir / filename
  let data ← IO.FS.readFile path
  let matrix ← parseData data
  return verify_rule matrix

#eval test_verify "data_1518.txt"
-- true

[Amir Livne Bar-on]

How comes compiling a large literal takes more time than hundreds of small ones? Is it due to optimizations that are allowed within values but not between values in the same module? I can't think of anything else that would make the runtime super-linear...

[Kyle Miller]

My guess is that it's spending time trying to optimize it, and it's not happy with the quarter of a million List.cons cells. It's going to compile to some code that calls the List.cons a whole lot.

[Mario Carneiro]

The compiler also isn't good at avoiding deep terms, in particular because it automatically puts expressions in A-normal form

[Mario Carneiro]

combine this with the fact that handling deep nested binders is quadratic and you are in for a bad time

[Kyle Miller]

Another approach is to break up the computation across multiple definitions. Here's the beginning of that, it defines rule_verified_0 through rule_verified_521, and it'll take 3-4 hours to complete... But it shouldn't run out of memory!

code

import Lean

open Lean Elab
open Std.Internal.Parsec
open Std.Internal.Parsec.String

def parseArray {α : Type} (p : Parser α) : Parser (List α) := do
  ws *> skipChar '['
  let arr ← many (ws *> p <* optional (ws *> skipChar ','))
  ws *> skipChar ']'
  return arr.toList

def parseData (data : String) : IO (List (List Nat)) := do
  match parseArray (parseArray digits) (String.mkIterator data) with
  | .success _ v => return v
  | .error _ err => throw <| IO.userError err

elab (name := includeStr) "def_nat_matrix " id:ident str:str : command => Command.liftTermElabM do
  let some str := str.1.isStrLit? | throwUnsupportedSyntax
  let srcPath := System.FilePath.mk (← MonadLog.getFileName)
  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
  let path := srcDir / str
  let data ← IO.FS.readFile path
  let matrix ← parseData data
  addDecl <| .defnDecl {
    name := id.getId
    levelParams := []
    type := mkApp (.const ``List [levelZero]) (mkApp (.const ``List [levelZero]) (mkConst ``Nat))
    value := toExpr matrix
    hints := .abbrev
    safety := .safe
  }
  Term.addTermInfo' id (mkConst id.getId) (isBinder := true)

def_nat_matrix data_1518 "data_1518.txt"

def allIdxAux {α : Type} (xs : List α) (f : Nat → α → Bool) (i : Nat) : Bool :=
  match xs with
  | [] => true
  | x :: xs => f i x && allIdxAux xs f (i + 1)

def allIdx {α : Type} (xs : List α) (f : Nat → α → Bool) : Bool :=
  allIdxAux xs f 0

def allIdx₂Aux {α β : Type} (xs : List α) (ys : List β) (f : Nat → α → β → Bool) (i : Nat) : Bool :=
  match xs, ys with
  | x :: xs, y :: ys => f i x y && allIdx₂Aux xs ys f (i + 1)
  | _, _ => true

def allIdx₂ {α β : Type} (xs : List α) (ys : List β) (f : Nat → α → β → Bool) : Bool :=
  allIdx₂Aux xs ys f 0

def verify_rule_y (M : List (List Nat)) (y : Nat) : Bool :=
  let rowy := M.get! y
  let rowyy := M.get! (rowy.get! y)
  allIdx₂ M rowy fun x rowx yx =>
    rowyy.get! (rowx.get! yx) == x

elab "kernel_rfl_true" : tactic => Tactic.liftMetaTactic1 fun g => do
  g.assign <| ← Meta.mkExpectedTypeHint (← Meta.mkEqRefl (mkConst ``true)) (← g.getType)
  return none

elab "mk_rule_verified_ys" : command => do
  for y in [0:522] do
    let id := mkIdent (Name.mkSimple s!"rule_verified_{y}")
    Command.elabCommand <| ← `(theorem $id : verify_rule_y data_1518 $(quote y) = true := by kernel_rfl_true)

set_option profiler true
mk_rule_verified_ys

[Mario Carneiro]

Out of time for today, but you can see my progress on equational#976. Turns out this has all the usual structure of a greedy construction, but I don't yet understand all the invariants. (@Terence Tao ?) One thing in particular which I'm not quite following is that the code seems to add things in "cycles", which implies something about an auxiliary property like "every partial assignment induces a directed graph where every vertex in the graph has positive in and out degree". (Or maybe in/out degree 1?) It would be great if someone could figure out the greedy invariants in the style of the 854 proof.

[Mario Carneiro]

A concrete theorem which I don't know how to prove without some additional invariant is that the construction proceeds by adding a cycle of 6 points $x_0 \stackrel{y}{\to} x_1 \stackrel{S^5y}{\to} \dots \stackrel{Sy}{\to} x_6=x_0$ whenever $\neg\exists z.\;x_0 \stackrel{y}{\to} z$ (where $x_0$ is one of the non-idempotents), but why is it the case that $x_i\stackrel{S^{6-i}y}{\to} z$ (for some $z\ne x_{i+1}$) isn't already in the graph?

[Terence Tao]

This is indeed the biggest obstacle to making this construction fully automated. One needs "enough" cycles passing through $x_0$ that, for any $y$ for which one wishes to define $y \diamond x_0$, that at least one of them has the property $x_i \not \stackrel{S^{6-i}y}{\to} z$ for all $i, z \neq x_{i+1}$, so that one can safely define this operation. Sometimes no such cycle is currently available and one has to first insert that cycle into the partial operation first before being able to define $y \diamond x_0$. In practice, if the magma is large enough and the cycles are sufficiently "disjoint" then one can do this, possibly after adding in a few more elements to make room, but it's hard to do it systematically. I have experimented with trying to formally create a greedy algorithm for this, but the amount of new elements and operations one has to add to "fix" any undefined operation is already about half of the size of the finite model, so verifying that the greedy construction iterates properly may well be of comparable difficulty to directly verifying the finite model.

[Terence Tao]

A key problem is that every cycle $x_0 \stackrel{y}{\to} x_1 \stackrel{S^5 y}{\to} x_2 \dots$ through a non-idempotent $x_0$ generates a further cycle $\dots x_2 \stackrel{x_1}{\to} x_0 \dots$ that passes through the same non-idempotent $x_0$. It turns out that this process can be made to loop back on itself in $J$ steps for some $J \geq 3$, though to avoid unwanted collisions, and to have enough cycles through $x_0$ available that one can always allocate one to a given $y$ to define $y \diamond x_0$, one needs $J$ to be moderately large (about 5 or so). Furthermore, these cycles will also generate a few other 2-cycles that also need to be added. The process does terminate and lead to the ability to define $y \diamond x_0$ for any given $y$, but it takes a remarkably large amount of effort to do so.

[Mario Carneiro]

So the way I would like to structure this is that we have some base behavior of the operation (the $xy=y$ rule, and most of the seed properties, including all the 2 cycles), which completely determines the value of all of the elements not involved in the greedy rule. The greedy rule itself should ideally be over the smallest possible "action space" because that reduces the number of cases to check (the proof that the initial seed is functional is already quite scary looking in my formalization, so if I can restructure it as a function instead of a relation that will make things much easier).

[Mario Carneiro]

If there is a deterministic process of cycle adding that loops back on itself, I think that should all be done in the same extension step. We can at least predict what happens in that case and prove that it loops back properly. The hard part is the greedy step where we take a "random" element and add it to the graph, since then we lose information about the structure we've built. The number of new elements in each step is not the issue (in fact adding more new elements in each step is a good thing because it reduces the number of steps), instead we need a description of what an obstruction looks like. Your code just solves all the greedy steps in order; is it just a coincidence that this works and a different order may get stuck?

[Mario Carneiro]

We could define a valid greedy step as one where $x_i \not\stackrel{S^{6-i}y}{\to} z$ for all $i, z \neq x_{i+1}$, but in that case the limit object will be one which is "stuck" such that all cycles are blocked. I did not understand your point about "one has to insert that cycle into the partial operation first", it sounds like you are modifying the seed in this step? So maybe this is the mechanism you are using to reorder things instead.

[Terence Tao]

Oh, this is a step that is not reflected in the final python code I uploaded, but rather in the trial-and-error process (across many versions of the python code, as well as many scratch paper and blackboard diagrams) in which I kept trying a seed, finding a collision, and then modifying the seed in an ad hoc manner to fix the problem.

In any event I think I now have a more high-level abstraction of the argument. Given a carrier $M$, define a suitable digraph to be a directed graph $G$ of edges $x \to x'$ on $M$ with the following axioms:

1. There is a bijection on the set of edges that maps each edge $x_0 \to x_1$ to a unique "successor" $x_1 \to x_2$ that starts at the final vertex $x_1$ of the original edge. (But there may also be non-sucessor edges emenating from $x_1$.) Hence every edge $x_0 \to x_1$ also has a unique "predecessor" $x_{-1} \to x_0$ (but there may be other edges entering $x_0$). We can then define a "good path" $x_0 \to x_1 \to \dots x_n$ in the graph in which each edge is the successor of the previous one, and similarly a "good cycle" $x_0 \to x_1 \dots \to x_{n-1} \to x_0$.
2. If $x_0 \to x_1 \to x_2$ is a good path, then $x_2 \to x_0$ is also an edge in the digraph.

In the case of finite 1518 magmas, there is an associated suitable digraph in which $x \to z$ if $z = L_y x$ for some $y$, and the successor of $x \to z$ is $z \to L_z^{-1} x$ (and the predecessor is $L_x z \to x$).

Because of finiteness, the suitable graph can be thought of as an edge-disjoint collection of good cycles, as each edge will belong to exactly one cycle. Note that we allow cycles $x \to x$ of length 1 (these will correspond to idempotents), as well as cycles $x \to z \to x$ of length 2. In practice, I was able to generate candidate suitable graphs by starting with a cycle that I wanted to have in the graph (to hold a desired counterexample), creating more edges by Axiom 2, completing those into cycles in some ad hoc process (guided by avoiding previous failures), and iterating until the cycles produced became 1-cycles (which iterate to themselves).

Now suppose we have selected a suitable digraph $G$ and also a bijection $S: M \to M$ with the property that $x \to Sx$ is in the diagraph for all $x$. Define a partial solution to be a partially defined operation $\diamond$ on $M$ obeying the following axioms:

1. If $$y \op x = z$$, then $x \to z$ is an edge in the digraph. In such cases we write $x \stackrel{y}{\to} z$.
2. If $x \to z \to w$ is a good path and $z \stackrel{y}{\to} w$, then $x \stackrel{Sy}{\to} z$. (By periodicity, we also get the converse implication for free: if $x \stackrel{Sy}{\to} z$, then $z \stackrel{y}{\to} w$).
3. If $x \to z \to w$ is a good path, then $w \stackrel{z}{\to} x$.
4. For any $x$, we have $x \stackrel{x}{\to} Sx$.

One can check that if a partial solution is total, then it obeys 1518, and that $S$ is indeed the squaring operation $Sx = x \diamond x$.

One can attempt to generate a seed partial solution by imposing Axioms 3,4 to create some initial operations, and then propagating them by Axiom 2. This construction is guaranteed to obey Axiom 1, but is not guaranteed to have $\diamond$ be a partial function: there can well be collisions in which we attempt to enforce $x \stackrel{y}{\to} z$ and $x \stackrel{y}{\to} z'$ for distinct $z,z'$. I do not have a general theorem that gives clean conditions for when such collisions can be avoided: I have relied on trial and error and python code (and some intuition about how "sparse" suitable digraphs are less likely to cause collisions) to do this.

Once one has a seed, one has to complete it to a total operation, by assigning values to $y \diamond x$ that are currently undefined. The easiest case is when $y$ and $x$ are both idempotent. Then we simply assign the right absorptive law $x \stackrel{y}{\to} x$, the addition of which does not break any axioms. However, one should not perform this step initially, but only at the end, because there are other completion steps that may require $y \diamond x$ to be assigned something other than the right absorptive law.

The hardest case is when $y,x$ are both non-idempotent. Here the only solution I had was to ensure that the initial seed already defines all these operations. This is one reason why I wanted to keep the set of non-idempotents as small as possible (there are 12 of them in the specific example, but I think I have a way to cut it down to 6).

A relatively easy case is when $y$ is non-idempotent and $x$ is idempotent. Here one can proceed if (a) there is a shift isomorphism $T: M \to M$ that preserves the partial solution and the suitable digraph; (b) One has $Sy = Ty$; and (c) one has $x \to T^{-1} x \to T^{-2} x \to \dots T^{-n+1} x \to x$ as a good cycle in the digraph. In this case one can set $T^{-i} x \stackrel{T^{-i} x}{\to} T^{-i-1} x$ for all integers $i$. The axioms (a), (b), (c) will ensure that this does not break any axioms or create any collisions. So I designed the digraph and the squaring map to have these symmetry assumptions.

Finally, there is the case where $y$ is idempotent and $x$ is non-idempotent. Here, the task is to find a good cycle $x \to x_1 \to \dots \to x_n \to x$ passing through $x_0 := x$, such that $y \diamond x_i$ is not defined for any $i$. Then one can set $x_i \stackrel{y}{x_{i+1}}$ for all $i$. This can be done if there are "enough" good cycles that are "spread out" in some way. It is in order to achieve this that the $J$ parameter in the python code had to become large, and this is major contributor to the large size of the magma.

I believe I have a slightly simpler construction of a digraph and squaring function that both leads to a smaller magma (it should be of size 144, if my calculations work out), but I will check it in python first (and also refactor the python code to reflect the above arrangemnt of the argument) before reporting it.

[Vlad Tsyrklevich]

Matthew Bolan said:

This is for its twin 476 and not 503, but that shouldn't make a difference

Finally got around to looking at and importing these, they didn't cause any issues.

[Matthew Bolan]

Do you plan to formalize the cohomology construction in general? I assume the order 65 example is a problem right?

[Matthew Bolan]

I can provide the needed tables to compress all these examples further if the construction itself gets formalized.

[Vlad Tsyrklevich]

I've got a host of others things in front of me right now, so I'm not planning to do it in the short-term. If you have the data though and it's fresh in your mind, it may be worth adding to that GitHub ticket.

[Vlad Tsyrklevich]

Matthew Bolan said:

I assume the order 65 example is a problem right?

Yes

[Matthew Bolan]

That one in particular has carrier $\mathbb Z / 5 \mathbb Z \times \mathbb Z / 13 \mathbb Z$, and operation $(x_1, x_2) \diamond (y_1, y_2) = (4x_1 + 2y_1, 5x_2+9y_2 + f(x_1,y_1))$, where $f$ is given by

this table

{(0, 0): 0,
(0, 1): 0,
(0, 2): 5,
(0, 3): 11,
(0, 4): 12,
(1, 0): 1,
(1, 1): 0,
(1, 2): 7,
(1, 3): 10,
(1, 4): 0,
(2, 0): 0,
(2, 1): 8,
(2, 2): 0,
(2, 3): 0,
(2, 4): 11,
(3, 0): 0,
(3, 1): 4,
(3, 2): 3,
(3, 3): 0,
(3, 4): 4,
(4, 0): 0,
(4, 1): 10,
(4, 2): 1,
(4, 3): 4,
(4, 4): 0}

[Matthew Bolan]

Matthew Bolan said:

1516 -> 1489 counterexample can be reduced from size 49 to size 35

If we are adding those other two we might as well also add this one.

[Vlad Tsyrklevich]

Oh, I had missed this in the backscroll.

[Terence Tao]

I reduced the size of the 1518 example to 232, down from the previous record of 438, by using a different type of starting cycle and making some different choices in iterating.
output2.txt
array2.py

The python code is now refactored to first construct the list of cycles and show it obeys the required axioms 1-4, and then start building the multiplication table from that list and checking that no collisions occur. This may be somewhat easier to formalize.

[Kyle Miller]

@Terence Tao This time I tried a base-256 encoding of each row of the matrix, since the Lean kernel has special support for Nat, so it's a way to do random-access arrays. This made it possible to verify a form of M[M[y][y]][M[x][M[y][x]]] == x in 22s, but it will still take a little work to prove that the calculation I did is what I'm claiming it's doing. (It's just to translate the verify_rule function into a proposition.) The data format is the same — it's assuming the file it's reading is just the array from your output2.txt file.

code

import Lean
import Batteries.Data.List

open Lean Elab
open Std.Internal.Parsec
open Std.Internal.Parsec.String

def parseArray {α : Type} (p : Parser α) : Parser (List α) := do
  ws *> skipChar '['
  let arr ← many (ws *> p <* optional (ws *> skipChar ','))
  ws *> skipChar ']'
  return arr.toList

def parseData (data : String) : IO (List (List Nat)) := do
  match parseArray (parseArray digits) (String.mkIterator data) with
  | .success _ v => return v
  | .error _ err => throw <| IO.userError err

-- assume each nat is ≤ 256
def rowToNat (row : List Nat) : Nat :=
  match row with
  | [] => 0
  | n :: ns => n + 256 * rowToNat ns

elab (name := includeStr) "def_nat_matrix " id:ident str:str : command => Command.liftTermElabM do
  let some str := str.1.isStrLit? | throwUnsupportedSyntax
  let srcPath := System.FilePath.mk (← MonadLog.getFileName)
  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
  let path := srcDir / str
  let data ← IO.FS.readFile path
  let matrix ← parseData data
  guard <| matrix.length < 256
  guard <| matrix.all (·.length < 256)
  addAndCompile <| .defnDecl {
    name := id.getId
    levelParams := []
    type := mkApp (.const ``List [levelZero]) (mkConst ``Nat)
    value := toExpr (matrix.map rowToNat)
    hints := .abbrev
    safety := .safe
  }
def_nat_matrix data_1518 "data_1518.txt"

elab "kernel_rfl" : tactic => Tactic.liftMetaTactic1 fun g => do
  let some (_, lhs, _) := (← g.getType').eq? | throwError "not an equality"
  g.assign <| ← Meta.mkExpectedTypeHint (← Meta.mkEqRefl lhs) (← g.getType)
  return none

elab "kernel_rfl_true" : tactic => Tactic.liftMetaTactic1 fun g => do
  g.assign <| ← Meta.mkExpectedTypeHint (← Meta.mkEqRefl (mkConst ``true)) (← g.getType)
  return none

def extract (matrix : List Nat) (row col : Nat) : Nat :=
  255 &&& ((List.get! matrix row) >>> (col * 8))

def IsTable (matrix : List Nat) : Prop :=
  let n := matrix.length
  ∀ x < n, ∀ y < n, extract matrix x y < n

instance : DecidablePred IsTable := by
  intro matrix
  unfold IsTable
  infer_instance

theorem data_1518_is_table : IsTable data_1518 := by decide +kernel -- or `decide!` on an older Lean

/-
`M[M[y][y]][M[x][M[y][x]]] == x` for all `x` and `y`.
-/
def verify_rule (M : List Nat) : Bool :=
  Nat.fold (init := true) 232 fun x _ b =>
    b && Nat.fold (init := true) 232 fun y _ b =>
      b && extract M (extract M y y) (extract M x (extract M y x)) = x

set_option profiler true
#eval verify_rule data_1518 -- 200ms

-- 21.3s
theorem verify_data_true : verify_rule data_1518 = true := by kernel_rfl_true

theorem verify_rule_correct (M : List Nat) :
    verify_rule M ↔ ∀ x < 232, ∀ y < 232, extract M (extract M y y) (extract M x (extract M y x)) = x := by
  unfold verify_rule
  sorry

def eq_47 (M : List Nat) : Prop := extract M 0 (extract M 0 (extract M 0 0)) ≠ 0
def eq_614 (M : List Nat) : Prop := extract M 0 (extract M (extract M 0 0) 0) ≠ 0
def eq_817 (M : List Nat) : Prop := extract M 0 (extract M (extract M 0 0) (extract M 0 0)) ≠ 0
def eq_3862 (M : List Nat) : Prop := extract M (extract M 0 (extract M 0 0)) 0 ≠ extract M 0 0

example : eq_47 data_1518 := by rintro ⟨⟩
example : eq_614 data_1518 := by rintro ⟨⟩
example : eq_817 data_1518 := by rintro ⟨⟩
example : eq_3862 data_1518 := by rintro ⟨⟩

[Mario Carneiro]

you also need to check that all the entries are less than 232 with this formulation

[Joachim Breitner]

Kyle Miller said:

This time I tried a base-256 encoding of each row of the matrix

Isn’t that pretty much what https://github.com/teorth/equational_theories/blob/6c65d0a0a0193ea88383f0234e5511e19b2f7142/equational_theories/MemoFinOp.lean does, or am I missing something here?

[Mario Carneiro]

the encoding is slightly different, since it's using powers of 2 and also using a list of nats instead of a single one

[Mario Carneiro]

it might be interesting to see whether memoFinOp can be sped up by using powers of 2 so that you can use shiftl instead of mul

[Joachim Breitner]

This was discussed before somewhere here. I believe it won't save much. My assumption is that the cost is kernel time, not the actual bignum operation, and if you use powers you then have to an extra mod or lt to clamp to the expected Fin range, so there is an extra step needed.

But I could be wrong, predicting performance is always dangerous. Shouldn’t be hard to adapt the existing code if someone is curious.

[Joachim Breitner]

Is list of nat an improvement over a single nat? Maybe to work around the issue with how lean represents huge nat literals in the C code (lean4#5771)? If so, should it be an RArray of Nat?

[Mario Carneiro]

there is already a mod involved in opOfTable

[Mario Carneiro]

and the t / n^i division in particular is one of the more expensive bignum operations you can do

[Mario Carneiro]

we're looking at numbers with a few thousand bytes at least, it should be measurable at that size

[Joachim Breitner]

Mario Carneiro said:

there is already a mod involved in opOfTable

Right – a div and a mod. With power of two you’d need a shift and an and and a mod or lt-check.

But you are right, it’s worth a try!

[Mario Carneiro]

the difference is that the mod will be of numbers around 5-30, rather than 2^25-2^900

[Mario Carneiro]

actually, the % n and Nat.mod_lt proof is already there in opOfTable

[Mario Carneiro]

that's the exact same check either way

[Joachim Breitner]

It’s not quite the same (or I’m confused) – the % n isn’t just a check, it also removes the “upper bits”, whereas in the power-of-two variant you (presumably) remove the upper bits after shifting using && (2^k-1) or % 2%k, and then still have to do one more operation to make lean accept it as a Fin n.

But I agree that it’s worth a try given the smaller numbers.

Also calculating the shift as i * k is likely cheaper than calculating the divisor n^i.

[Mario Carneiro]

You can do all the bit selection using bit operations: (t >>> a*w) &&& !(1 <<< w) and then % n or if x < n then x else 0 at the end

[Mario Carneiro]

ideally you would calculate w and !(1 <<< w) beforehand since they are constants

[Joachim Breitner]

Ok, no confusion then :-)

[Terence Tao]

Here is a modification to the cohomology method that may help with the Lean verification of examples such as the order 169 refutation of 1076 -> 2294. Here we work with operations of the form $(x,s) \diamond (y,t) = (x \diamond y, as + bt + f(x,y))$ where $x,y,s,t$ all take values in the same finite field $F_p$ of prime order (e.g., $F_{13}$ in the case of the order 169 example), the base operation $x \diamond y = a' x + b' y$ is also linear, and $f: F_p \times F_p \to F_p$ is a function. Previously we were viewing this as a linear algebra problem over $p^2=169$ unknowns, which appears to be challenging for Lean (though no problem for e.g., SAGE). But notice that $f(x,y)$ can also be interpreted as a bivariate polynomial of degree at most $2p-2$ (with coefficients in $F_p$; actually the only monomials that show up are of the form $x^i y^j$ with $0 \leq i,j \leq p-1$, thanks to Fermat's little theorem). Also, the derivative operator takes homogeneous polynomials of degree $d$ to homogeneous polynomials of degree $d$. So we can split up into "isotypic subspaces" and assume without loss of generality that $f$ is a homogeneous polynomial of degree $d$ for some $0 \leq d \leq 2p-2$. Now there are only $\min( d+1, 2p-1-d)$ unknown coefficients; the previous 169-dimensional linear algebra problem has been split up into 25 linear algebra problems of dimensions between 1 and 13. I'm suspecting that one should already see counterexamples at relatively low degrees, e.g., d=2,3,4, in which case the entire magma can be defined by a low degree polynomial and verification within Lean should actually be quite easy (maybe even doable by ring).

For fixed $d$ one could now test all primes $p$ (and all coefficients $a,b,a',b'$) at once by viewing the problem as an abstract linear algebra problem with coefficients polynomial in some indeterminates $a,b,a',b'$ obeying some polynomial identities, and apply some Grobner basis algorithm.

[Matthew Bolan]

Alright, that seems easy enough to do, I'll get on it.

[Terence Tao]

A cheap option would be to take the existing counterexample $f: F_{13} \times F_{13} \to F_{13}$, express it as a bivariate polynomial, split it into homogeneous components, and extract the lowest degree component that isn't identically zero. This should also be a counterexample.

[Terence Tao]

Actually, it might not be the lowest degree component that holds the counterexample, because the 2294 derivative operator could vanish on that component. One wants the lowest degree component for which the 2294 derivative operator doesn't vanish.

[Matthew Bolan]

Right now I'm going to just intersect the $Z^2$ I currently calculate with the space of degree $d$ polynomial functions. I can also do the Groebner basis computation pretty easily, but I think I want to start from scratch for that one.

[Kyle Miller]

Mario Carneiro said:

you also need to check that all the entries are less than 232 with this formulation

Ok, I added the couple lines of code to check this, which is the trivial part of this exercise.

On top of this, one should add

def M : Fin 232 → Fin 232 → Fin 232
  | ⟨x, hx⟩, ⟨y, hy⟩ => ⟨extract data_1518 x y, data_1518_is_table x hx y hy⟩

and then restate the verification theorems in terms of this M, but I think the underlying kernel computation theorems should still be in terms of data_1518 to avoid unnecessary Fin juggling. Anyway, the question of whether this could be checked computationally in Lean is unblocked now, right? Am I missing anything?

[Kyle Miller]

Joachim Breitner said:

Isn’t that pretty much what https://github.com/teorth/equational_theories/blob/6c65d0a0a0193ea88383f0234e5511e19b2f7142/equational_theories/MemoFinOp.lean does, or am I missing something here?

Sorry, I'm not very familiar with what's been done in this project. I can say that there are three performance considerations that led to my design:

1. I use Nat rather than Fin for the kernel verification, leaving the Fin interface for main final theorem statements. There's no need for the kernel to spend time manipulating the Fin constructor, or to do unnecessary mod operations to make sure values are in range. These aren't necessary for the computation, so let's prove them outside the computation.
2. I used a List Nat encoding rather than a single Nat because the numbers were big enough that, in my experience, bignum arithmetic really does start to become noticeable. I didn't do any performance comparisons here, since my goal was creating a proof of concept. If it were a single Nat, we're working with 55k base-256 digit numbers, and individual binary shifts are, sure, O(1), but it will take copying up to 55kB of data. That's a lot of memory overhead just for accessing the matrix, and a quick back-of-the-envelope calculation suggests that this would be at least 11GB of memory traffic just to do all the matrix accesses. Not terrible, but at least by having a list of Nats this goes down to about 50 MB of copying.
3. I used powers of two because division and modulo are relatively expensive bignum operations, and the numbers are big enough where I'm starting to worry. Shifting is more expensive than I'd like (it takes scanning over the entire number) but at least 255 &&& . should only look at limb zero, vs . % 256, which is another linear scan.

[Matthew Bolan]

Ok for 1076 we can take $f$ to be degree $3$

[Terence Tao]

So this should lead to an extremely compact description of the magma operation on $F_{13} \times F_{13}$ as a cubic polynomial for which 1076 should be easy to verify (and 2294 easy to refute) in Lean.

[Matthew Bolan]

On the carrier $\mathbb Z / 13 \mathbb Z \times \mathbb Z / 13 \mathbb Z$ the law is $(x_1, x_2) \diamond (y_1, y_2) = (5 x_1 + 9 y_1, 5 x_2 + 9 y_2 + x_1y_1^2 + 11x_1^2y_1 + x_1^3)$

[Terence Tao]

Does it violate both 2294 and 4435?

[Matthew Bolan]

Yes

[Terence Tao]

OK. This should be straightforward to formalize, I opened equational#981 for this.

[Terence Tao]

If you already have the values of $x_1,x_2,y_1,y_2$ for the counterexamples for 2294 and 4435 that may help the formalization process a little.

[Terence Tao]

I think I'll also update the relevant section of the paper, this is an extremely concrete example to illustrate the cohomology method

[Douglas McNeil]

Lunchtime in my time zone, so I can catch up. How widely applicable are these approaches? Could there be improved and/or simplified refutations for already handled pairs? Can't remember if it's in the current plans or not, but I know collecting statistics on how different techniques performed was mooted at one point.

[Matthew Bolan]

Terence Tao said:

If you already have the values of $x_1,x_2,y_1,y_2$ for the counterexamples for 2294 and 4435 that may help the formalization process a little.

I'm having to undo some coordinate transforms I did to feed it into FME, but I believe both violations are at $x=(0,0), y=(1,0)$.

[Terence Tao]

It feels like this technique could be automated. Though even the preliminary task of identifying the linear magma solutions to each equation hasn't yet been completed (related to equational#364), so constructing linear extensions of linear magmas by polynomial cocycles for all 4694 equations would be a certain amount of work. But it seems doable to me, given enough effort.

[Matthew Bolan]

I actually wasted quite a bit of time these past few days partially automating the process of identifying the linear magma solutions.

[Terence Tao]

One nice thing about low degree polynomials is that if an identity fails, it tends to fail nearly everywhere (Schwartz-Zippel lemma, applied to polynomial identity testing), so actually in retrospect one could have picked $x,y$ at random and already have a good chance of landing on a counterexample. But certainly having an explicit pair can't hurt.

[Terence Tao]

If you can get to the point where you can automatically identify the smallest non-trivial linear magma over a finite field for each of the 4694 equations, that would be a nice addition to Equation Explorer. I would be curious to know what proportion of the refutations in the finite implication graph can be resolved either by linear models, or by linear extensions of linear models, I am guessing the percentage to be extremely high (say 98% or so).

[Matthew Bolan]

I ran into the annoying issue that in order to compute the non-commutative linear models, what I want to do amounts to computing a Groebner basis in the free (non-commutative) algebra over $\mathbb Z$. I found this website which lists computer algebra packages and which non-commutative rings they support, but the ones I have access to don't work out. The maple package JanetOre sounds promising though, I just don't have easy access to maple at the moment.

Without the computation over $\mathbb Z$, I still think we can get away with only computing Groebner bases in free algebras over fields, provided the package we are using is able to express the basis in terms of the original generators. This way we can see which primes need to be invertible to guarantee the polynomials we care about lie in the ideal. Unfortunately, I again could not figure out how to do this (but I'm pretty sure this approach should be possible with one of the systems I have access to, I did not try very hard).

[Terence Tao]

I suspect the commutative models over a finite field should already suffice for a very large fraction of refutations.

[Matthew Bolan]

In contrast, the commutative situation is very simple since sage can do groebner bases over $\mathbb Z$, my cohomology program already has this as a subroutine.

[Matthew Bolan]

Terence Tao said:

I suspect the commutative models over a finite field should already suffice for a very large fraction of refutations.

Yes, but as far as I can tell many implications have not been fully checked for (non-commutative) linear immunity, and I'd like to do this. It's annoying because it should be possible for most implications (though there's a good chance the Groebner basis computation does not terminate for some, I think we lose this guarantee in the non-commutative setting), there just doesn't seem to be any one black box I can use for the computation.

[Terence Tao]

Actually, for the purposes of the paper, could you run your algorithm for the 1110->1629 refutation with p=5, and $(a,b)=(a',b')=(3,-1)$? This should be an even simpler example than the p=13 1076 example.

[Matthew Bolan]

That one needs degree $5$.

[Terence Tao]

Would you be able to give explicit coefficients?

[Terence Tao]

That already is slightly lowering my expectations for the method for the broader implication graph though. I was vaguely hoping that the quadratic and cubic examples would already be quite successful in clearing out implications. Though perhaps it is premature to extrapolate from N=2 data points...

[Matthew Bolan]

Ah, I was confused by something and now I am less confused. I think we cannot actually exclude monomials where the exponent on $x$ or $y$ is greater than $p-1$, since replacing them using Fermat's little theorem would violate homogeneity.

[Vlad Tsyrklevich]

Just using Kyle's method above for faster indexing, the 1076 counterexample finishes in <5s, no maxHeartbeats changes.

[Matthew Bolan]

The law is $(x_1, x_2) \diamond (y_1, y_2) = (3x_1 - y_1, 3x_2 - y_2 + y_1^5 + x_1y_1^4 + x_1^2y_1^3 + 3x_1^3y_1^2 + 3x_1^4y_1)$

[Terence Tao]

@Matthew Bolan Ah, I missed that, thanks for the correction.

[Vlad Tsyrklevich]

Right now I just shimmed it into the current architecture that resolves the refutation by decide! which seems to be ~2x slower for 1518 than Kyle's Nat.fold check and I haven't had a chance to look at that yet.

[Terence Tao]

I assume you mean $x_1,y_1$ instead of $x, y$?

[Matthew Bolan]

yes,

[Matthew Bolan]

and there is an obvious transcription error, one second

[Terence Tao]

I'll double check it in python

[Matthew Bolan]

Yeah, I've actually already done that, so any errors remaining are just transcription ones. I believe it is now corrected though.

[Mario Carneiro]

Kyle Miller said:

Anyway, the question of whether this could be checked computationally in Lean is unblocked now, right? Am I missing anything?

No I think you are right, this should solve the issue

[Kyle Miller]

@Vlad Tsyrklevich In case it helps, the reason for Nat.fold was that I saw that it had good properties for kernel reduction, and I worried that the Decidable instance might use something like docs#Nat.all, which seemed like it might be slower because it would have to defer reducing the match in && (but I didn't measure anything!)

[Terence Tao]

OK, the quintic counterexample for 1110->1629 works, and x = (1,0) for instance serves as a specific counterexample. FME

[Mario Carneiro]

PS: I feel like this thread should have been split ages ago, half of the project has now happened on it

[Terence Tao]

Fair enough; I'll open threads for the specific finite implications remaining to be either formalized or resolved.

[Terence Tao]

OK, I've spun off the 677 and Lean+Duper topics. I think the task of formalizing the large counterexamples for 1076 and 1518 can be continued here, as it seems we are very close to completing it.

[Terence Tao]

Is it worth developing a tactic for verifying magma laws for bytecode arrays? In principle all the finite magma refutations could pass through this tactic which might make it faster.

[Matthew Bolan]

I have something resembling a general solver for small $d$ working now. Unfortunately it is pretty slow once $d$ gets bigger than $3$. I am not taking advantage of the fact the problem is linear in the coefficients of the cocycle at all, so probably I can improve that. In the meantime it revealed that there is a quadratic example for 1516 not implying 1489 on $F_7 \times F_7$, $(x_1,x_2) \diamond (y_1,y_2) = (6x_1+2y_1, 4x_2 + y_2 + 5y_1^2 + x_1y_1)$

[Vlad Tsyrklevich]

Terence Tao said:

In principle all the finite magma refutations could pass through this tactic which might make it faster.

There's already something like this on main, memoFinOp. It may make sense to unify FinitePoly with All4x4Tables to make it easier to convert all memoFinOp users to the new format, as FinitePoly doesn't define operation tables.

[Vlad Tsyrklevich]

@Zoltan A. Kocsis (Z.A.K.) I noticed that FinitePoly only has magmas of size $\le 5$, and when I tried deleting the FinitePoly refutations, I noticed something odd. There were refutations that went missing that were refuted by 2x2 magmas that All4x4Tables also knows about. But those refutations are just not being generated. That seems surprising to me because I don't see anywhere in generate_lean.py that is looking at the FinitePoly tables to avoid generating those refutations, so I'm not sure what's happening. Do you know off the top of your head why this might be happening?

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

Vlad Tsyrklevich said:

Zoltan A. Kocsis (Z.A.K.) I noticed that FinitePoly only has magmas of size $\le 5$, and when I tried deleting the FinitePoly refutations, I noticed something odd. There were refutations that went missing that were refuted by 2x2 magmas that All4x4Tables also knows about. But those refutations are just not being generated. That seems surprising to me because I don't see anywhere in generate_lean.py that is looking at the FinitePoly tables to avoid generating those refutations, so I'm not sure what's happening. Do you know off the top of your head why this might be happening?

Not off the top of my head (it's been a while since I looked at the project at all), but am happy to take a look tomorrow!

[Vlad Tsyrklevich]

I spent a lot of time trying to make this into a nice macro and seem to have made everything worse. I'm out of my depth in meta-programming. Trying to use Lean's native parsing introduced a huge overhead (~15s), it seems to be faster to do finOpTable "[[1,2...} instead of finOpTable [[1,2,... but I'm sure I could just be doing something foolish. One thing I'm surprised by is that IsTable takes ~15s which is almost as long as verifying the actual satisfiability. Does that sound right to you @Kyle Miller ?

native parsing example

def rowToNat (row : List Nat) : Nat :=
  match row with
  | [] => 0
  | n :: ns => n + 256 * rowToNat ns

def extract (matrix : List Nat) (row col : Nat) : Nat :=
  255 &&& ((List.get! matrix row) >>> (col * 8))

def IsTable (n : Nat) (matrix : List Nat) : Prop :=
  ∀ x y : Fin n, extract matrix x y < n

instance decidableIsTable {n matrix} : Decidable (IsTable n matrix) := by
  unfold IsTable
  infer_instance

def extractWrapper (n : Nat) (matrix : List Nat) (h : IsTable n matrix) (row col : Fin n) : Fin n :=
  ⟨extract matrix row.val col.val, h row col⟩

def parseNats (size : Nat) (stx : Array Syntax) : TermElabM (List Nat) := do
  stx.toList.mapM fun elem => do
    let nats := elem[1].getArgs.filter fun x => x.isNatLit?.isSome
    guard <| nats.size == size
    return rowToNat (nats.toList.map (fun x => x.isNatLit?.get!))

elab "finOpTable" "[" xs:term,* "]" : term => do
  let size := xs.getElems.size
  guard <| size < 256
  let matrix : List Nat ← parseNats size xs.getElems
  let table ← matrix.foldrM
    (fun elem acc => mkAppM ``List.cons #[mkNatLit elem, acc])
    (mkApp (mkConst ``List.nil [Level.zero]) (mkConst ``Nat))
  let istable := mkApp2 (mkConst ``IsTable) (mkLit (.natVal size)) table
  let mv ← mkFreshExprMVar istable
  discard <| withCurrHeartbeats <|
    Tactic.run mv.mvarId! do Lean.Elab.Tactic.evalTactic (← `(tactic| decide!))
  return mkApp3 (mkConst ``extractWrapper) (mkLit (.natVal size)) table mv

example :
    finOpTable [[0,1],[1,0]] = fun a b : Fin 2 => [[0,1],[1,0]][a]![b]! := by
  funext a b; revert a b; decide

[Kyle Miller]

@Vlad Tsyrklevich I'm not sure there's any benefit to using Lean's native parsing here — the matrices are just data, and all that matters is that the resulting loaded table is a witness. You could even make it load from a base 64 blob or something, if you want the Lean source to be shorter. (At least, these are my own opinions as a relative outsider to this project.)

Using mkAppM is going to be slower than using toExpr like I did. mkAppM goes through a more general procedure with a lot more calculation.

I noticed that IsTable is slow to check too, but it was an acceptable amount of time so I didn't look into it. Best I can say is that it's making use of random access all the way, rather than say iterating over the rows of matrix and checking the condition, which would be more efficient. You'd have to back that up with a proof — this alternative formulation can go into decidableIsTable using decidable_of_iff, which is a way to set which algorithm to use for a given proposition.

[Vlad Tsyrklevich]

equational#991 adds support for Kyle's implementation, it is much easier to look at the first commit to avoid the spam from re-generating counter-examples.

[Joachim Breitner]

Did anyone already check if using RArray instead of List makes a difference? (Assuming the project is already on a new enough lean, if not the code can be copied from https://github.com/leanprover/lean4/pull/6070 easily temporarily.)

[Vlad Tsyrklevich]

Just ran a very quick local test, and it does not seem to, when testing with the largest counterexample we have.

[Joachim Breitner]

thanks, guess the lists are small enough for this to not matter.