Szemerédi Regularity Lemma

Stream: general

[Yaël Dillies]

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?

[Oliver Nash]

Congratulations!

[Oliver Nash]

Are you planning on migrating this to master?

[Yaël Dillies]

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]

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]

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

[Bhavik Mehta]

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]

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]

This paper? Indeed sounds pretty related!

[Mauricio Collares]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

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]

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

[Johan Commelin]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Mauricio Collares]

https://twitter.com/wtgowers/status/1459271456865591298

Happy to see that Szemerédi’s regularity lemma has been formalized. It has also been done (independently) in Lean by Yaël Gillies and Bhavik Mehta — the latter a PhD student of mine I’m proud to say (but strictly no credit for this is due to me — I heard about it after the fact). https://twitter.com/isaprover/status/1457393417202274306

- Timothy Gowers (@wtgowers)

[Eric Rodriguez]

Yaël Gillies :/

[Yaël Dillies]

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]

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]

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]

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

[Yaël Dillies]

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

[Aaron Anderson]

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]

Okay, split off in #12988

[Yaël Dillies]

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

[Kyle Miller]

@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]

And the namespace?

[Yaël Dillies]

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

[Aaron Anderson]

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

[Yaël Dillies]

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