GREEDY-GREEDY HYBRID: Refute 1516->255

Stream: Equational

[Pietro Monticone]

@Marco Petracci, @Lorenzo Luccioli and I have just started working on the task equational#820 and we are trying to understand as much as possible about the informal proof in the blueprint.

We have a few questions:

1. In the blueprint (see here) the initial construction for the base magma is done over the carrier $\mathbb{Z}$. This construction has already been formalised (see the exact lines here) with the only difference that the carrier in this case is the free group over $\mathbb{N}$ (A := FreeGroup Nat). Could we just proceed with the blueprint proof substituting $\mathbb{Z}$ with A?
2. The elements of $G'$ in the blueprint seem to be treated sometimes as triples and sometimes as quadruples. Which one is correct? It seems to us that treating them as triples (i.e. ignoring the fourth component when present) suffices, but we are not 100% sure.
3. In the last part of the proof of Proposition 17.5 (see here) we find the sentence "Iterating these procedures over a well-ordering of $G' \times \mathbb{Z} \times \mathbb{N}$ [...]". Is this a typo? Shouldn't it be $G'$ or $\mathbb{Z} \times \mathbb{Z} \times \mathbb{N}$ instead?

[Terence Tao]

1. It should be fine to use FreeGroup Nat (with relevant changes in notation), I don't think the abelian nature of the model was particularly important for the rest of the construction.
2. Sorry, that was a remnant of an older, more complicated construction. You can ignore the fourth component whenever it appears.
3. Yeah, it should just be $G'$ here (this is again a remnant of a previous construction. Presumably one should use https://teorth.github.io/equational_theories/docs/equational_theories/Mathlib/Order/Greedy.html#exists_greedy_chain to do this part of the construction (so an explicit well-ordering is not needed.)

Feel free to update the blueprint to match the formalization as needed.

[Pietro Monticone]

UPDATE: Opened draft PR. We have 3 sub-tasks left.

[Terence Tao]

Great news! Aside from the issues raised earlier, were there any mathematical issues you encountered? Or ways in which the blueprint proof could have been made easier to formalize?

[Lorenzo Luccioli]

Regarding the blueprint proof of Corollary 17.7, we noticed that it requires refining the construction from Proposition 17.6. However, we realized that the construction in Proposition 17.5 already suffices to refute 255, without any explicit modifications. Specifically, we can use  x₀ := (*, 0, 0) ∈ G' ⊆ A × A × ℕ, where * ∈ FreeGroup ℕ = A is the empty word, the first 0 is the image of 0 through the injection ℕ → A and the second 0 is just the natural number.
By plugging x₀ into 255, we obtain the following sequence of equalities:

((x₀ ◇ x₀) ◇ x₀) ◇ x₀ = ((S x₀) ◇ x₀) ◇ x₀ = (* ◇ x₀) ◇ x₀ = * ◇ x₀ = *,

where  * ≠ x₀ . Thus, 255 is refuted without requiring further refinement. This approach seemed more straightforward to formalize.

As far as Proposition 17.5 is concerned, we initially faced some challenges in mapping the informal proof to the formal structure of the greedy extension. In particular, the informal proof suggests adding infinitely many elements to the partial solution even at intermediate steps to achieve infinite surjectivity ( ∀ b : ℤ, x : G', {y : G' | L b y = x}.Infinite). However, maintaining the finiteness of the partial domain seems crucial.

To address this, here is the workaround we adopted:

• Define a quantity based on the current partial solution, specifically the cardinality of the set of  a ∈ A  for which  L a y  is already defined for some  y .

• This quantity serves two purposes: it limits the number of elements added at each step (ensuring finiteness) and ensures that the sets  {y : G' | L b y = x} are sufficiently large. This ultimately allows us to prove their infiniteness in the limit.

We incorporated this condition into the structure PartialSolution and used it to complete most of the proof. The main task remaining is constructing Next, which extends a PartialSolution to include a new pair (d, g) ∈ A × G'  where the function is not yet defined. I am actively working on this and hope to finalize it in a few days.

Further details and comments about this workaround are included in a comment in the draft PR.

[Terence Tao]

Nice shortcut at the end of the argument. Yes, you are right, the addition of infinitely many elements at each stage of the greedy algorithm is technically incompatible with our usual greedy algorithm formalism, but the workaround you found looks good to me.

[Lorenzo Luccioli]

Quick report about the state of this task.

We have good news and bad news.

Good news first: the skeleton of the implementation is complete, there are a few sorries left (which are very unlikely to be problematic), and we plan to complete them in the next few days.

Now for the bad news. Formalizing the proof of Proposition 17.5 made some inconsistencies with the informal proof come to light. In particular we found 3 of them, from less to more serious:

1. Around the middle of the proof we define the image of two elements $c’$ and $y$ relying on the surjectivity of $L_a$, I think there is a missing step here where we should use the surjectivity a second time. More details are in a small comment in the code, however this is already fixed in the formalization and in the blueprint.
2. When we add the image of a new pair to the greedy construction we need to prove that the equation 1516 (L_{S y} LₓLₓy = x) continues to be satisfied, given that all the operations are well defined. If the pair that we are adding anew is (x, y) then the proof goes as intended, however if the new pair is one of (x, Lₓy) and (S y, LₓLₓy) then I’m not sure how to proceed. More details here.
3. After adding the extra elements that we use for the infinite surjectivity, we need to prove again that 1516 is satisfied. In this case we already circumvented the issue found in 2., the problem is in the actual proof. In fact, in the proof it is stated that for elements of the form $c_{w,c'}$ we already have that $L_{c_{w,c'}} w = c'$. This is true if the image of $c_{w,c’}$ and $w$ has been added in the first part of the proof; however, it is not necessarily true if it has been added in the second part (where we add the extra elements for the infinite surjectivity). Moreover, I think that it is not even possible to enforce it during the construction, so I fear that it is not only an issue of the implementation, but the proof actually needs to be adapted somehow. More details here.

From tomorrow and for the rest of the week I will be unable to work on the project, and I’m not sure how much time I will be able to spend on it in the following weeks. It would be great if somebody could tackle the subtasks mentioned above. 

PS. I added the label 🛑 Problem 🛑 in the code to identify where these main problems are.

[Terence Tao]

Sorry about all the issues with the blueprint, I am working now on a better version, fixing a number of confusing typos and also making some tweaks to the construction. Will keep you updated.

[Pietro Monticone]

Thanks a lot!

[Terence Tao]

OK, I have updated the blueprint to provide a clearer explanation of the greedy construction, in particular splitting the proof of what was previously Proposition 17.5 into several smaller pieces, and describing in more detail what a partial stage of the iteration looks like, and also correcting some typos. In particular, the inductive hypothesis is set up so that one only ever needs to test the $(x,y)$ pair when verifiying $L_{Sy} L_x L_x y = x$, because we will show that whenever $L_x y$ is well-defined, then the entirety of $L_{Sy} L_x L_x y$ is well-defined.

I realized though that one key property of the construction, namely that $c_{y,b} \neq c$ for all $b$ and $y=(a,c,n)$, was somehow omitted from the construction (though it was still used in a key step), which was the reason why we had the second component $c$ of the triple $(a,c,n)$ in the first place (the point being that $L_c (a,c,n)$ is not initially frozen by the construction, and is at one's disposal to set later in order to get the infinite surjectivity property). In putting that in I realized that one has to strengthen the base magma axioms very slightly (so that a certain equation not only has one solution, but at least two), but as detailed in the new blueprint, it should just be a matter of enlarging the seed a little bit.

[Lorenzo Luccioli]

The implementation of the new proof is now almost complete!
This time, things went much more smoothly—partly because the new proof is more detailed and formalization-friendly, and partly because I’m now more familiar with the required structures and was able to reuse parts of the old code.

I found just a small thing to adjust in the proof of Lemma 17.5. When constructing the useful element  $c_{y, b}$, we currently require that $c_{y, b} \neq a, b, c$. However, to ensure we can exclude $c$ as well, I think we need a stronger version of Corollary 17.4, stating that the equation $R_a c = b$ has at least 4 solutions (instead of just 3, as before). Fortunately, the existing implementation was easy to adapt—this just required changing a constant.

The only remaining task is updating the lemma base2. This is about the base magma: the previous implementation required just one solution for $L_a R_a b = b$, but now we need two. I haven’t really looked into this yet, since I’m not too familiar with the base magma implementation, so it might be faster for someone who has already worked on it to handle this part.

[Terence Tao]

That's great progress!

Looking at the Lean proof of base2 (which I think was largely done by @Bernhard Reinke ), I see the setup is different from in the blueprint, in that the carrier was taken to be FreeGroup Nat rather than ℤ. But I think one just needs to add a new variable x₇ := x 7, add (x₇⁻¹, x₇^2), (x₇^3, x₇) to E0, and use both x₆ * a and x₇ * a to get the two solutions (one has to show that x₆ * a and x₇ * a are distinct, but this should be easy).

[Bernhard Reinke]

Yes, I think this is the way to proceed. I could implement it if you want (but I guess I would need write access for b-reinke for the PR fork) but feel free to give it a shot yourself!

[Lorenzo Luccioli]

Thank you very much! With those tips, I managed to make the change myself in a matter of minutes. Now the proof is completely sorry-free!

[Lorenzo Luccioli]

I’ll clean up the PR a bit before merging—some golfing, merging master, and a few small tweaks to the blueprint.

[Pietro Monticone]

I’ll review the latest changes and set the PR ready to merge later today

[Pietro Monticone]

Done equational#1054

[Terence Tao]

In hindsight this validates @Bernhard Reinke 's call to work in FreeGroup Nat rather than ℤ; ℤ is a conceptually simpler object for human mathematicians to understand, but from Lean's point of view, FreeGroup Natis the simpler structure to work in (in particular, I see that proving x₆ * a ≠ x₇ * a was almost just a single simp call in FreeGroup Nat). (The construction in the blueprint involved choosing two somewhat arbitrary integers to be the analogue of x₆ and x₇, but actually verifying all the required properties would be some tedious norm_num type calculation. Still not super difficult, but it seems the FreeGroup Nat framework made this sort of tweaking of proof near-painless).

[Terence Tao]

A small observation: here it was possible for one contributor to look at a proof written by another contributor, and suggest the necessary changes to a third contributor, who could then implement them easily. This is an ability which is quite possible for formally verified proofs, but significantly more challenging for an informal proof, because there are many more opportunities for misunderstandings, typos, or other problems to be created in this chain of communication. So this is one aspect of the proof writing process where the formalized approach is already superior to the informal one.

[Shreyas Srinivas]

Terence Tao said:

A small observation: here it was possible for one contributor to look at the proof written by another contributor, and suggest the necessary changes to a third contributor, who could then implement them easily. This is an ability which is quite possible for formally verified proofs, but significantly more challenging for an informal proof, because there are many more opportunities for misunderstandings, typos, or other problems to be created in this chain of communication. So this is one aspect of the proof writing process where the formalized approach is already superior to the informal one.

I'm currently writing a section on the scale issues of formal projects. I will note this message down for this section. But I might have some questions about how the sequence of events unfolded.

[Terence Tao]

The Feb 4 comments in this thread tell most of the story, but I will try here to reconstruct the backstory, that I pieced together from the Zulip history (but perhaps @Bernhard Reinke can correct any details).
)
I think @Bernhard Reinke initially formalized a refutation of 1516->1489 using a noncommutative greedy construction (originally due to @Pace Nielsen). At some point I used this construction to build a "base model" for a refutation of 1516->255 (which would contain Bernhard's magma as a submagma); but I decided to switch from a noncommutative construction to a commutative one for "simplicity" when writing the blueprint, and also I needed an additional axiom that a certain equation always had at least one solution. But it was possible to adapt the greedy argument to do this by making the seed slightly larger, and Bernhard kindly formalized all of this, though keeping with the noncommutative construction rather than following the blueprint closely.

Later, @Pietro Monticone and @Lorenzo Luccioli formalized the rest of the argument in the blueprint, where they located some moderately serious issues with the blueprint proof that, among other things, required a strengthening of the additional base model axiom so that the equation in question now had at least two solutions rather than at least one. In principle, this was just a matter of enlarging the seed yet again, but because the formalization was not tracking the blueprint perfectly, this wasn't obvious initially. But I was familiar with how the commutative construction related to the noncommutative one, and I could read the relevant lines of Bernhard's proof without needing to inspect the hundreds of other lines, so I could fairly quickly point out the necessary changes, even without direct access to the PR to implement them.

[Bernhard Reinke]

I think overall this is a good summary. One technical detail: the two extra properties of Corollary 17.4 were dealt with in two slightly different ways:

Property (ii) needed an additional extension step (basically the noncommutative version of Lemma 17.3). The generality of exists_greedy_chain was very convenient for this change. The new version of property (ii) requires four instead of three solutions, this was easily adjustable by changing some constants.

Property (iii) could be enforced by a larger seed. For the new version, one could simply take an even larger seed as @Terence Tao pointed out.