Finishing the formalization of anti-implications

Stream: Equational

[Pace Nielsen]

The last 9 or 10 formalizations appear to be slow going. This semester I got a very bright undergraduate doing some research with me, and I was wondering if it would be worthwhile to have him work on finding different ways to disprove those implications. If so, could I get a list of which disproofs would help the most? If not, are there other aspects of the project that would benefit from a fresh set of eyes? [I did set him the task of creating the full Euler diagram for identities with 2 or fewer uses of the magma operation. Depending on how that goes, I may up it to 3 or fewer.]

[Terence Tao]

The four equations that produce outgoing anti-implications that still need to be formalized for the infinite implication graph are 1323, 1516, 1729, and 1692. All of them are claimed by one of the participants, so perhaps this might be a good thread to report on progress and whether they could use any assistance on the theory side.

[Shreyas Srinivas]

I’ll pick up 1729 after returning from vacation

[Shreyas Srinivas]

Which should be this week

[Aaron Hill]

I just finished formalizing all of the 1692 non-implications from https://github.com/teorth/equational_theories/issues/607 (I have @[equational_result] building with no sorrys). I'm planning to do some cleanup before I pr it, as it's pretty messy at the moment

[Bruno Le Floch]

Naive question @Aaron Hill : this github issue mentions 6 implications, but the equation explorer also shows the implications to 23, 63, 1922, 3522, 4118 as unproven. Are they consequences of the other non-implications you prove?

[Vlad Tsyrklevich]

Looking at the graphiti (blue are currently open conjectures) you can see that the 6 equations from the GitHub issue are all at the top of the Hasse diagram, e.g. if 1692 refutes those 6, it also refutes everything below (since the entries towards the top are the 'most general', e.g. they admit the most models.)

[Shreyas Srinivas]

I have started the formalisation of equation 1729 vs 817 in equational#1063 . I'll be working on this as when I can squeeze some time in.

[Terence Tao]

Glad to see the formalization of the 1692 non-implications now landed at equational#1069! Thanks to @Aaron Hill for the huge effort, and @Pietro Monticone for the additional golfing and optimization!

[Pietro Monticone]

It can be optimized quite a lot more, but I don’t have enough time today.

[Aaron Hill]

Let me know if you have any questions about the way I wrote the file, or if you'd like me to help with golfing it further

[Terence Tao]

I'd be interested in any reporting of experiences you had with formalizing various aspects of the proof, and which steps proved unexpectedly challenging or tedious to formalize (and which ones were easier than expected). I'd be especially interested if you had any suggestions for writing human proofs in a way that makes Lean formalization easier or more enjoyable.

[Alex Meiburg]

When you look at the proof on GitHub -- and it doesn't show you because the file is too big to display! :)
Wow! :D

[Pietro Monticone]

Reduced by other 400 lines https://github.com/teorth/equational_theories/commit/dc00332b13a72930502bd467a8c9f8c3a74f487d

[Amir Livne Bar-on]

Hi! Adding here that the anti-implication from 1323 is now formalized:
https://github.com/teorth/equational_theories/pull/1021/
(Worked on it bit by bit once in a while on weekends, and didn't follow Zulip)

I would appreciate reviews on this, since I'm new at Lean, and proof formalization in general. I mostly didn't know the best tactics to use, and there definitely will be areas that can be clarified or simplified.

The proof doesn't follow the blueprint exactly in two respects:
(a) Using $\mathbb{Z}/2 \times F_{\mathbb{N}}$ instead of $\mathbb{Q}^\times$, as usual in our proofs
(b) The greedy construction adds an infinite number of elements in each step, but the formal proof only tracks a single element of each orbit
In retrospect I'm not sure (b) was the right choice, we can instead track the full set keep an auxiliary condition that the set of generators in the free group is finite. This might be simpler.

In addition I re-used the variant of FreshGenerator that I used for equation 63 - an isomorphism $F \mapsto (\mathbb{Z}, +)$ that counts the occurrences of the fresh generator, rather than a projection $F \mapsto F$. I found this easier to use for proofs where this is sufficient. Now it's in the common module.

Another change is adding the fact that the map $x \mapsto x^n$ on the free group is injective. This is strictly more general that the implication we have now $x^n = 1 \implies x = 1$, but the proof is different and more complicated. I didn't remove the old one.

(I must say that the ReducedWords module is very nice to work with, it provides tools that allow both low-level and high-level calculation with the free group, and contains interesting mathematical content)

[Bernhard Reinke]

Nice work! I think we could start upstreaming ReducedWords to mathlib, in particular with your addition of the injectivity of power maps. I guess a good first step would be to upstream the dependencies in our Mathlib folder. I haven't really polished them yet. If someone with more upstreaming experience wants to have a look at it, feel free to do so!

[Bernhard Reinke]

I think I started PRs for most of the dependencies. Should we mark the lemmas in our code base with the corresponding PR?

[Shreyas Srinivas]

I’ll try to push my progress as it exists in a few hours (or maybe tuesday afternoon) from now for 1729

[Shreyas Srinivas]

I don’t see the point of marking lemmas with PRs since git blame can always find it

[Bernhard Reinke]

Ok, I have opened a PR (#22639) for the upstream of ReducedWords to mathlib. In the end, I reduce the infinite order to the injectivity of the power function, as the old proof interacted badly with the translation to additive groups.

[Shreyas Srinivas]

Partial update on 1729. It took me some time to get working on this PR due to my day job. WIP in PR equational#1098. The first major step is theorem 18.1 that I think I can finish soon (a few hours of work).

[Terence Tao]

It may be possible to distribute up the work after that among more people. For instance, after Theorem 18.1, one has to introduce two separate objects SM, N and establish some basic properties about them, and that could be done independently; and once N is defined, one can also independently introduce the right multiplication operators R'_a and their basic properties.

[Shreyas Srinivas]

I think it can begin independently. Theorem 18.1 is fairly self contained

[Terence Tao]

I was thinking of using the same file Equation1729.lean for all of the relevant code, but don't want to cause a merge conflict. If you think Theorem 18.1 can be formalized soon I can then try to add stubs for the next few lemmas and definitions. If it might take some time, another option is to get your current PR into a mergeable state and then work independently off of that file .

[Shreyas Srinivas]

Just refactored the 1729 PR. Since there are conceptually two distinct pieces, if someone wants to work on the magma construction itself, it should be possible to do this without merge conflicts on equational#1098

[Shreyas Srinivas]

Since I am working off a branch on the main repository, it should be possible to make a PR to the branch eq1729

[Terence Tao]

OK I have just started a separate PR at equational#1100 to set up the basic structure of the argument. There may need to be a small merge of the Equation1729.lean file at some point but this should be straightforward. Once it passes CI, I'll start creating issues for various lemmas and definitions used in the proof for people to work on independently.

[Shreyas Srinivas]

I think in order to make this work it is easier to work off the PR 1098 and add the stubs to the MagmaConstruction.lean file

[Shreyas Srinivas]

In fact, I would even split up the stub into smaller files

[Shreyas Srinivas]

The properties of SM can be in their own file.

[Terence Tao]

I just merged #1100. How about if you incorporate the stub into #1098 with your proposed refactoring and then put that up as a preliminary PR (with multiple sorries)? Then we can all work on fresh PRs on different components. (There are more components to the 1729 blueprint that aren't in the stubs I already uploaded, but what is there is perhaps enough for now, and I can add the others later once the file structure stabilizes.)

[Shreyas Srinivas]

I’ll make a PR in 3 hours which will organise the file structure and then merge that into main. Then I will base equational#1098 on top of this new main

[Shreyas Srinivas]

Other PRs can do the same with different files

[Shreyas Srinivas]

I just noticed that the project is stuck at toolchain v4.14.0-rc3 (CC : @Pietro Monticone is the update script turned off for some reason?)

[Shreyas Srinivas]

There are some breakages to fix in the Magma Law theory section

[Pietro Monticone]

You might want to take a look at equational_theories.FreeMagma in this bump PR?

It's the only broken file I have left because I have never touched it.

In particular, it fails at

@[simp] theorem map_forks {α β} (m : FreeMagma α) (f : α → β) :
    (fmapHom f m).forks = m.forks := by simp [fmapHom]; induction m <;> simp [forks, *]

and at

@[simp] def map_toList {α β} (m : FreeMagma α) (f : α → β) :
    (fmapHom f m).toList = m.toList.map f := by simp [fmapHom]; induction m <;> simp [*]

returning unsolved goals.

[Shreyas Srinivas]

I am seeing much more extensive breakage in the auto generated folders

[Shreyas Srinivas]

let's hold off on the update

[Pietro Monticone]

Are you bumping to the latest toolchain version? The bump PR mentioned above is quite old (v1.16.0-rc2).

[Terence Tao]

How decoupled is the toolchain update from the formalization of 1729? One could perhaps stick with an old toolchain for now for the purposes of getting some initial momentum on the 1729 formalization, and defer the problem of updating the toolchain to later if it isn't urgent (though I suppose it will need to be done eventually if we want to upstream stuff to Mathlib).

[Shreyas Srinivas]

We can work on it independently. Hence my suggestion that we leave the update aside for now

[Shreyas Srinivas]

I also think I got rid of most of the errors (mostly by pure luck)

[Shreyas Srinivas]

Also I think we can set out tasks for formalising pieces of it. I will stub out until theorem 18.2

[Shreyas Srinivas]

I am outdoors at the moment but will return to a machine soon

[Shreyas Srinivas]

I think attempting to upgrade this code will prove too tedious. Let's not update this for now.

[Shreyas Srinivas]

I just spent several hours trying to fix all the errors and there are still some errors showing up

[Shreyas Srinivas]

We might have more success upgrading in individual toolchain level increments

[Shreyas Srinivas]

So apparently downgrading the toolchain of the local copy of a repository is confusing business*. I simply replaced my local copy.

#general > Running lake cache without updating the lean toolchain @ 💬

[Shreyas Srinivas]

The outline is almost ready. Just need to fix some declarations in the blueprint

[Shreyas Srinivas]

Once this PR passes CI, it can be merged.

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/pull/1098

[Shreyas Srinivas]

Merged. @Terence Tao : I merged your stubs into this PR

[Shreyas Srinivas]

Now I will continue with smaller PRs to fill out the sorrys