## Stream: general

### Topic: Szemerédi Regularity Lemma

#### Yaël Dillies (Oct 20 2021 at 16:16):

Bhavik and I are thrilled to announce that we now have a sorry-free proof of Szemerédi Regularity Lemma!
It shows that any big enough graph is close to random graphs with the same amount of edges. It is often dubbed "the most important lemma of extremal graph theory".

This was my summer internship, started mid-June. Our work lives at branch#szemeredi.

Next steps might be the Triangle Removal Lemma, the Blowup Lemma, the Erdős-Stone Theorem, and maybe even Roth's Theorem?

Congratulations!

#### Oliver Nash (Oct 20 2021 at 16:30):

Are you planning on migrating this to master?

#### Yaël Dillies (Oct 20 2021 at 16:45):

Ahah! La question qui fâche.
I am indeed planning on PRing this (and #9795 is the first step), but I don't want to set too high of an expectation because the proof is calculatory. Now, we're PRing the non SRL-specific bits. Later, we may try convincing maintainers that our pile of calc is worth having.

#### Yaël Dillies (Oct 20 2021 at 16:56):

Note, this is related to the cap-set problem. Cap-set is a Roth in finite fields, with a stronger conclusion to compensate.

#### Johan Commelin (Oct 20 2021 at 17:04):

Great work! Does that mean that we can revive https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/hedetniemi.20branch?

#### Bhavik Mehta (Oct 20 2021 at 17:16):

No, I don't think so! As far as I know, SRL doesn't make that specific construction easier (although it would be nice to get back to that)

#### Mauricio Collares (Oct 20 2021 at 20:31):

That's fantastic! I am particularly interested in the extremal combinatorics applications, but this also opens the door for graphons and therefore for Sah's recent upper bounds on diagonal Ramsey numbers.

#### Yaël Dillies (Oct 20 2021 at 21:02):

This paper? Indeed sounds pretty related!

#### Mauricio Collares (Oct 20 2021 at 21:34):

Yes, this one! But I can't tell if it uses graphons in an essential way (taking limits, say) or if it's just convenient notation for finite calculations. Either way, one application of SzRL is to show that the space of graphons with the cut norm is compact, as in Section 5 of https://web.cs.elte.hu/~lovasz/analyst.pdf.

#### Angeliki Koutsoukou Argyraki (Oct 21 2021 at 18:02):

This is fantastic @Yaël Dillies @Bhavik Mehta ! You might be interested to know that (just this week!) @Chelsea Edmonds @Lawrence Paulson and myself have just finished Szemerédi's regularity lemma in Isabelle/HOL and we are close to finishing Roth's Theorem on arithmetic progressions too. We started in July and we can keep you updated on our progress if you like! As soon as we polish it a bit first, our formalisation will appear on the Archive of Formal Proofs.

#### Angeliki Koutsoukou Argyraki (Oct 21 2021 at 18:15):

Angeliki Koutsoukou Argyraki said:

This is fantastic Yaël Dillies Bhavik Mehta ! You might be interested to know that (just this week!) Chelsea Edmonds Lawrence Paulson and myself have just finished Szemerédi's regularity lemma in Isabelle/HOL and we are close to finishing Roth's Theorem on arithmetic progressions too. We started in July and we can keep you updated on our progress if you like! As soon as we polish it a bit first, our formalisation will appear on the Archive of Formal Proofs.

PS. also it looks like we are all in Cambridge! :smile: it would be great to meet you! :smile:

#### Shing Tak Lam (Oct 21 2021 at 18:30):

Angeliki Koutsoukou Argyraki said:

Angeliki Koutsoukou Argyraki said:

This is fantastic Yaël Dillies Bhavik Mehta ! You might be interested to know that (just this week!) Chelsea Edmonds Lawrence Paulson and myself have just finished Szemerédi's regularity lemma in Isabelle/HOL and we are close to finishing Roth's Theorem on arithmetic progressions too. We started in July and we can keep you updated on our progress if you like! As soon as we polish it a bit first, our formalisation will appear on the Archive of Formal Proofs.

PS. also it looks like we are all in Cambridge! :smile: it would be great to meet you! :smile:

Btw I don't know if you follow the #Geographic locality stream, but we're meeting every Wednesday 3 to 6, MR11 in the CMS.

#### Bhavik Mehta (Oct 21 2021 at 20:20):

Angeliki Koutsoukou Argyraki said:

This is fantastic Yaël Dillies Bhavik Mehta ! You might be interested to know that (just this week!) Chelsea Edmonds Lawrence Paulson and myself have just finished Szemerédi's regularity lemma in Isabelle/HOL and we are close to finishing Roth's Theorem on arithmetic progressions too. We started in July and we can keep you updated on our progress if you like! As soon as we polish it a bit first, our formalisation will appear on the Archive of Formal Proofs.

What a great coincidence! We're working on Roth too :)

#### Angeliki Koutsoukou Argyraki (Oct 21 2021 at 21:05):

Bhavik Mehta said:

Angeliki Koutsoukou Argyraki said:

This is fantastic Yaël Dillies Bhavik Mehta ! You might be interested to know that (just this week!) Chelsea Edmonds Lawrence Paulson and myself have just finished Szemerédi's regularity lemma in Isabelle/HOL and we are close to finishing Roth's Theorem on arithmetic progressions too. We started in July and we can keep you updated on our progress if you like! As soon as we polish it a bit first, our formalisation will appear on the Archive of Formal Proofs.

What a great coincidence! We're working on Roth too :)

this is really cool! :) When I first got the idea in June to formalise this I was a bit surprised to see that this important theorem had not been done in Isabelle/HOL so far but didn't know you were starting it in Lean! :) I am wondering how much more difficult it would be to formalise Szemeredi's theorem -the generalised version of Roth, for any k.

#### Bhavik Mehta (Oct 21 2021 at 21:08):

Yeah, we were originally planning to do Szeremedi's theorem itself but as we both had other projects going on, we stuck to just SRL.

#### Yaël Dillies (Oct 21 2021 at 21:08):

We still have it on our radar, but the project will be more the size of LTE or sphere eversion than a casual summer internship.

#### Johan Commelin (Nov 04 2021 at 12:59):

@Yaël Dillies Did you know that Roth is already mentioned in a comment in mathlib? https://github.com/leanprover-community/mathlib/blob/d219e6bb4426e1e8977af11a991f36a0bbd91c87/src/number_theory/liouville/liouville_with.lean#L25

#### Mauricio Collares (Nov 04 2021 at 13:00):

That's another theorem from Roth, I think. The one provable with SzRL is about three-term arithmetic progressions in positive-density sets.

#### Mauricio Collares (Nov 04 2021 at 13:00):

https://en.wikipedia.org/wiki/Roth%27s_theorem_on_arithmetic_progressions

#### Johan Commelin (Nov 04 2021 at 13:04):

Aah, ok. Thanks for the info. I don't really know this stuff.

#### Yaël Dillies (Nov 04 2021 at 13:36):

Yup, I should have made it clear that what I was talking about wasn't THE Roth theorem.

#### Yaël Dillies (Nov 04 2021 at 13:38):

And I can now safely announce that we (= mostly Bhavik) have formalized Roth's theorem on arithmetic progressions as well! This involves

• The triangle counting lemma
• The triangle removal lemma
• The corners theorem
• Roth's theorem per say

Yaël Gillies :/

#### Yaël Dillies (Mar 27 2022 at 10:21):

After a long while in the limbs of the PR queue, the first few PR from our project finally got in. This means that we're reaching the point of SRL-specific constructions.

#### Yaël Dillies (Mar 27 2022 at 10:25):

I just opened four PR, two of which are SRL-specific:

• #12957 (+139, -0) Graph uniformity and uniform partitions
• #12958 (+42, -0) Energy of a partition
• #12962 (+156, -0) Numerical bounds
• #12982 (+172, -0) Cliques and triangles

#### Yaël Dillies (Mar 27 2022 at 10:44):

There are a few questions which I left unanswered:

• Where should SRL go? We could dump it all in one 3k lines file, but that doesn't sound great, so Bhavik and I decided on a folder. But what should this folder be? This deserves a poll.
• What do we want to namespace and how? I've currently put stuff in theszemeredi namespace.
• How much of the numerical facts do we want to inline. They theoretically all could, but further calculations are unreadable and slow enough on their own.
• Do we want a file for cliques and a file for triangles? If we opt for a file for triangles, then we could have combinatorics.simple_graph.triangle.basic, combinatorics.simple_graph.triangle.counting, combinatorics.simple_graph.triangle.removal.

All of this keeping in mind that we're planning on doing (part of) Density Hales-Jewett and Szemerédi's theorem this summer.

#### Yaël Dillies (Mar 27 2022 at 10:47):

/poll Where should Szemerédi's regularity lemma go?
combinatorics.simple_graph.szemeredi.
combinatorics.simple_graph.regularity.
combinatorics.szemeredi.
combinatorics.regularity.

#### Yaël Dillies (Mar 27 2022 at 10:48):

cc @Bhavik Mehta, @Aaron Anderson, @Kyle Miller

#### Aaron Anderson (Mar 27 2022 at 14:34):

If I open a file on cliques, I expect to see basic Ramsey theory, not work towards the triangle removal lemma. Thus I'd probably recommend separating out triangles.

#### Yaël Dillies (Mar 27 2022 at 17:28):

Okay, split off in #12988

#### Yaël Dillies (Mar 28 2022 at 09:07):

@Kyle Miller, what's your opinion on the folder name?

#### Kyle Miller (Mar 28 2022 at 09:14):

@Yaël Dillies I think Aaron's suggestion of combinatorics.simple_graph.regularity seems good, but I don't really have a strong opinion.

#### Yaël Dillies (Mar 28 2022 at 09:14):

And the namespace?

#### Yaël Dillies (Mar 28 2022 at 22:11):

@Aaron Anderson, regularity is way too vague as a namespace. It could be szemeredi_regularity (my personal favorite) or simple_graph.regularity.

#### Aaron Anderson (Mar 28 2022 at 22:47):

Either of those are good (I was assuming `simple_graph.regularity').

#### Yaël Dillies (Mar 31 2022 at 09:54):

Aaron, here's the handout we followed. It uses the name ε-uniform. SRL.jpg
Bhavik could tell you more about where it comes from.

Last updated: Dec 20 2023 at 11:08 UTC