FINITE: The Lean+Duper implications

Stream: Equational

[Terence Tao]

The following implications are proven using Lean+Duper (mostly using the fact that injectivity and surjectivity are equivalent on finite carriers), but not by pure Lean:

• 467 x = y ◇ (x ◇ (x ◇ (y ◇ y))) implies 2847 x = ((x ◇ (x ◇ x)) ◇ x) ◇ x (Human proof)
• 1133 x = y ◇ ((y ◇ (z ◇ y)) ◇ x) implies 1167 x = y ◇ ((z ◇ (y ◇ y)) ◇ x) (Human proof)
• 1167 implies 1055 (R)
• 1167 x = y ◇ ((z ◇ (y ◇ y)) ◇ x) implies 1096 x = y ◇ ((x ◇ (z ◇ y)) ◇ x) (Human proof)
• 1167 implies 1112 (R)
• 1167 implies 1133 (R)
• 1167 implies 1721 (R)
• 1167 implies 1897 (R)
• 1167 implies 1668 (R)
• 1167 implies 1701 (R)
• 1167 implies 1958 (R)
• 1167 implies 4615 (R)
• 1441 x = (x ◇ y) ◇ (x ◇ (x ◇ x)) implies 4067 x ◇ x = ((x ◇ x) ◇ y) ◇ x (Human proof)
• 1443 x = (x ◇ y) ◇ (x ◇ (x ◇ z)) implies 3055 x = (((x ◇ x) ◇ y) ◇ x) ◇ x (Human proof)
• 1681 x = (y ◇ x) ◇ ((x ◇ x) ◇ x) implies 3877 x ◇ x = (y ◇ (x ◇ x)) ◇ x (Human proof)
• 1701 x = (y ◇ x) ◇ ((z ◇ x) ◇ x) implies 1035 x = x ◇ ((y ◇ (x ◇ x)) ◇ x) (Human proof)

(R) - redundant

Also, reachable by the same method:

• 1516 x = (y ◇ y) ◇ (x ◇ (x ◇ y)) implies 255 x = ((x ◇ x) ◇ x) ◇ x (Human proof)

A Graphiti for all these equations is here, but it appears that "show unknowns and conjectures" is not working currently for some reasion.

It's possible that these could all be handled by hand, but perhaps there is an automated way to decompile the Duper portion of the Lean proofs? (See also equational#935.)

[Terence Tao]

Something very strange: 1113->1167 is listed as a conjecture in Conjectures.leanand "proven" as Finite.Equation1133_implies_Equation1167 in https://leanprover.zulipchat.com/user_uploads/3121/3oZXvUh5RSEFTzPmV-VJT-SV/DuperConjectures1.lean , but is actually refuted https://teorth.github.io/equational_theories/implications/show_proof.html?pair=1113,1167&finite . We should get to the bottom of this.

[Matthew Bolan]

Isn't the duper conjecture about 1133 and not 1113?

[Terence Tao]

OK. So now Equation Explorer is reporting that 1133 is in fact known to be equivalent to 1167, so perhaps some of the conjectures are actually redundant. (Or is the equivalence only conjectural? Hard to tell.)

[Matthew Bolan]

It's listed as conjectural for me.

[Terence Tao]

From the Graphiti of the 1167 cluster it seems that we only need to establish one implication, 1167 -> 1096, to resolve all the outbound implications.

[Terence Tao]

It's listed as equivalent in https://teorth.github.io/equational_theories/implications/?1167&finite even when "Treat conjectures as unknown" is checked, so there may be a bug here.

[Matthew Bolan]

Ah. I had "hide equivalent equations" unchecked, in which case it also shows up highlighted in yellow in the "Unknown" column.

[Matthew Bolan]

It seems like a bug that it is not highlighted in the equivalent equation list.

[Terence Tao]

I'm now a little bit suspicious of the 17 Lean+Duper implications, particularly 1133->1167, as they are resolving an unusually large number (291) of additional implications on the dashboard (basically creating a large equivalence class). This could well be the case, but perhaps it is worth getting human proofs of the 1133 <-> 1167 equivalence at least, as well as 1167 -> 1096.

[Amir Livne Bar-on]

Regardless of the typo, the 1113 refutation uses 1167=>2000 which is by superposition calculus and shouldn't be counted in the finite graph IIUC

[Terence Tao]

But that's a positive implication and hence true for both the infinite and finite graphs.

[Amir Livne Bar-on]

Oh right :face_palm:‍

[Vlad Tsyrklevich]

There may indeed be some lack of transitive reduction in the conjectures I added. What you're seeing is a bug/unexpected behavior in the equation explorer, it does not respect 'Treat conjectures as unknown' when computing equivalence classes.

[Vlad Tsyrklevich]

The high number of implicit conjectures is to be expected since the conjectures for 1133/1167 have a lot of transitive implications due to expanding an equivalence class.

[Vlad Tsyrklevich]

Terence Tao said:

It's possible that these could all be handled by hand, but perhaps there is an automated way to decompile the Duper portion of the Lean proofs?

You can export the term using Lean's show_term, but I'm not sure if this long-term maintainable, and it also doesn't solve 1516->255 so it may be worth just trying to Leanify the vampire proofs again.

[Vlad Tsyrklevich]

Terence Tao said:

"show unknowns and conjectures" is not working currently for some reasion.

This is my bug, it only shows unknowns, and I figured conjectures would be highlighted but without arrows when navigating from equation explorer. I should change the label in graphiti to reflect that.

[Vlad Tsyrklevich]

Confirmed that the only strictly necessary conjectures from 1133/1167 is 1167=>1096, not sure why I had missed that last time. So that brings down the explicit conjectures to 7.

[Amir Livne Bar-on]

Looking at the Duper proofs of 1167=>X in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/481257624, many of them go through 4689 (spelled "eq2693" in DuperConjectures1.lean). This was transitively reduced to the conjecture 1167=>4615.

Here's a proof for that one:

Equation 1167 is $L_y L_{z \diamond Sy} = I$, while equation 4615 is $L_{Sx} = L_{z\diamond x}$. For $x$ s that are squares $x=Sa$ we have $L_{z \diamond x} = L_a^{-1}$, which is independent of $z$ so 4615 holds.

But every element in 1167 is a square: $S x = L_x x$, so $x = L_{z \diamond Sx} Sx$ for any $z$. We can take for example $a = L_{Sx \diamond Sx} Sx$ for the above.

[Terence Tao]

Vlad Tsyrklevich said:

Confirmed that the only strictly necessary conjectures from 1133/1167 is 1167=>1096, not sure why I had missed that last time. So that brings down the explicit conjectures to 7.

How is 1133->1167 implied by the other conjectures?

[Vlad Tsyrklevich]

1096 implies 1133 and 1167 in the general graph

[Amir Livne Bar-on]

There's a bit of an inefficiency in this area, a lot of equations from these conjectures (1035, 1112, 1133, 1167, 1096) are simple rewrites of 1202 but only 1096 is proven to be equivalent to it

[Terence Tao]

Right but 1096->1133 and 1096<->1167 doesnt obviously imply 1133->1167

[Vlad Tsyrklevich]

Oh, duh. I had misread the graph, and had double checked my thinking earlier by running extract_implications outcomes --hist but had forgotten to run lake build so the output wasn't updated.

[Terence Tao]

To complete the human proof of 1167 -> 1096:

As noted by @Amir Livne Bar-on , 1167 implies that $L_{z \diamond x}$ does not depend on $z$ (this is essentially 4689), and that squaring is surjective, hence invertible on finite magmas. Meanwhile, 1096 claims that $x = L_y L_{x \diamond (z \diamond y)} x$. Hence $L_{x \diamond (z \diamond y)} = L_{S^{-2} z \diamond (z \diamond y)} = L_{L_{S^{-2} z} L_{S^{-1} z \diamond S S^{-2} z} y} = L_y$ thanks to 1167. So now $L_y L_{x \diamond (z \diamond y)} x = L_y x$ is independent of $z$, thus $L_y L_{x \diamond (z \diamond y)} x = L_y L_{x \diamond (y \diamond y)} x = x$ as required by a further application of 1167.

[Amir Livne Bar-on]

The properties of finite 1167 and 1133 magmas are even nicer. Equation 1133 is the related $L_y L_{y \diamond (z \diamond y)}=I$, and both satisfy $L_y^{-1} = L_{\tilde{y}}$ for $\tilde{y}=y \diamond Sy$. Substituting $z=\tilde{y}$ into both equations gives $L_y^{-1}=L_y$. And both have square roots by the argument above.

[Amir Livne Bar-on]

Looking at the Duper proof for 1133 => 1167, it uses the equality $L_{(z \diamond y) \diamond y} = L_{z \diamond y}$ as an intermediate step. This is not hard to show (a single application of 1133) but I don't see immediately how to derive 1167 or 1202 from this.

[Terence Tao]

How do you get that square roots exist for finite 1133 magmas? With this I can complete the proof. Since $L_y = L_y^{-1}$, 1167 is equivalent to $L_{z \diamond Sy} = L_y$. But by the intermediate step, $L_{z \diamond Sy} = L_w$ where $w = (z \diamond Sy) \diamond Sy$. By the intermediate step again together with $L_w = L_w^{-1}$, $L_w^2 w = w = L_{z \diamond Sy} Sy = L_w Sy$, hence by left-cancellability $Sy = L_w w = Sw$. If square roots exist then $y=w$ and now we are done: $L_{z \diamond Sy} = L_w = L_y$.

[Terence Tao]

1441 -> 4067 is easy. Write $\tilde C x = x \diamond Sx$, then 1441 asserts that $R_{\tilde Cx} R_y x = x$. Setting $y=Sx$ we get $x = S\tilde Cx$, so by finiteness $\tilde C Sx = x$. Replacing $x$ with $Sx$ in 1441 we conclude $R_x R_y Sx = Sx$ which is 4067.

1681 -> 3877 is similar: write $Cx = Sx \diamond x$, then 1681 asserts $R_{Cx} L_y x = x$. Again setting $y=Sx$ yields $x=SCx$ hence $x = CSx$, and on replacing $x$ with $Sx$ in 1681 one obtains 3877.

[Terence Tao]

1443 -> 3055: Clearly 1443 implies 1441, hence 4067 by the previous implication, so that 3055 simplifies to $x = Sx \diamond x$. Meanwhile, 1443 also implies $x = S(x \diamond (x \diamond z))$. On taking square roots and using $S \tilde C = x$, we obtain $x \diamond (x \diamond z) = \tilde Cx$. Appying this with $z = Sx$ we conclude $L_x \tilde Cx = \tilde Cx$, hence on replacing $x$ with $Sx$ we get $L_{Sx} x = x$ as required.

1701 -> 1035: This is similar, we simplify to $x = x \diamond Sx$, while 1701 gives $x = S((z \diamond x) \diamond x)$ hence $(z \diamond x) \diamond x = Cx$, so $R_x Cx = Cx$, so $R_{Sx} x = x$ as required.

[Terence Tao]

1113 -> 1167: By previous reductions, it suffices to show that squaring is surjective. Using the intermediate step $L_{(z \diamond y) \diamond y} = L_{z \diamond y}$ we have $L_{R_y^2 z} y = R_y^3 z = R_y^2 z$ and hence $y = L_{R_y^2 z} L_{R_y^2 z} y = S R_y^2 z$, giving the surjectivity.

[Amir Livne Bar-on]

Terence Tao said:

How do you get that square roots exist for finite 1133 magmas?

It follows from the explicit form of $L_y^{-1}$: since $Sx=L_x x$ we have $x = L_{\tilde{x}} Sx$

[Terence Tao]

Yeah but I couldn't see why $\tilde x$ depended only on $Sx$ and not on $x$ (in contrast to the 1167 situation). But in any event I found a different way to show that square roots exist, see above (I'm writing it up in the blueprint now).

[Terence Tao]

opened equational#985, equational#986 to formalize these implications (and the blueprint version will land shortly).

Wasn't able to make much progress on the remaining implication 467 -> 2847. Clearly the $L_y$ are surjective, hence invertible. If one considers the reflected magma operation $x \tilde \diamond y = L_x^{-1} y$ one finds that this new law obeys equation 437, x = x ◇ (y ◇ (y ◇ (x ◇ y))), but there doesn't seem to be all that much known about those magmas either (and 2847 becomes really weird when written in this new operation). I'll leave it to others to try to decipher the Duper proof here.

[Amir Livne Bar-on]

I almost have it: putting $x=Sy$ in 467 gives $Sy = y \diamond (Sy \diamond (Sy \diamond Sy))$. By left-cancellation, $y = Sy \diamond SSy$ and squaring is invertible. Denoting the square root operation $Rx = x \diamond Sx$, equation 2847 is $x = (Rx \diamond x) \diamond x$, or taking into account that all elements are squares, $Sx = (x \diamond Sx) \diamond Sx = Rx \diamond Sx$.
Putting $Rx$ and $x$ into 467, we get $Rx = x \diamond (Rx \diamond (Rx \diamond Sx))$ and by left cancellation $Sx = Rx \diamond (Rx \diamond Sx)$.

[Amir Livne Bar-on]

Finishing up: setting both variables to $Sx$ in 467 we have $Sx = Sx \diamond (Sx \diamond x)$. And then setting them to $Sx$ and $Rx$ we get $Sx = Rx \diamond (Sx \diamond (Sx \diamond x)) = Rx \diamond Sx$.

[Terence Tao]

Great! Now that all of the (reduced) set of Lean+Duper implications have fairly short human proofs, I have replaced the original formalization task, equational#935, with three smaller tasks, equational#985 equational#986 equational#987, to formalize subsets of them that are in similar clusters.

They all rely on the key fact that for functions for a finite set to itself, surjectivity is equivalent to injectivity. Is this already in Mathlib or in the project? It seems to me that outside of that one lemma, all the proofs should be quite straightforward to formalize by hand.

[Andrew Yang]

docs#Finite.injective_iff_surjective

[Terence Tao]

Ack! I was trying to move the Lean+Duper conjectures into individual files in ManuallyProved and ended up breaking the build (and also my local Lean installation). For some reason, the conjectures which compile just fine in Conjectures.lean no longer compile when placed in say the end of https://github.com/teorth/equational_theories/blob/main/equational_theories/ManuallyProved/Equation1516.lean with errors like

error: ././././equational_theories/ManuallyProved/Equation1516.lean:1322:47: unknown identifier 'G'
error: ././././equational_theories/ManuallyProved/Equation1516.lean:1322:99: unexpected token ':'; expected command

I will try to repair my own local Lean build to the point where I can diagnose what the problem is, but if someone can spot the issue before that, that would be great. I thought importing equational_theories.EquationalResult would suffice for moving the files, but this seems to be inadequate for some reason.

[Pietro Monticone]

Fixed here https://github.com/teorth/equational_theories/pull/1002

[Terence Tao]

OK, thanks to @Pietro Monticone 's fix, the move has been successful. The remaining 8 unformalized implications (which, when resolved, will imply 300 more!) are now located in individual files within the ManuallyProven directory (with ManuallyProven.lean already updated), so that to complete any of  equational#985 equational#986 equational#987 one now just has to replace the conjectures there with theorems, following the proof or blueprint link provided. They should all be relatively easy to formalize, being basically just a sequence of rewrites (and some have statements) together with some version of docs#Finite.injective_iff_surjective, and establishing one of these may be a good task for a more casual participant who wants to practice their Lean skills.

Later today I will similarly make files for 1323 and 1516 in the main project. These are much more complex proofs and it may make sense to break the proofs into smaller pieces first that can be independently formalized.

[Terence Tao]

476 and 1516 were in fact easy to formalize: equational#1009 equational#1010

[Terence Tao]

the cluster 1133 and 1167 is now also formalized equational#1011 , which should remove most of the outstanding implications from the finite graph shortly.