## Stream: graph theory

### Topic: Szemerédi's Theorem

#### Yaël Dillies (May 18 2021 at 17:28):

Bhavik and I are gonna formalise Szemerédi's Theorem over the summer. Wish us luck!

#### Yaël Dillies (Jun 13 2021 at 21:26):

@Mauricio Collares, we're currently working on Szemerédi' Regularity Lemma here. There's not much to do at the moment as Bhavik is carrying the main induction and it's a bit one-goaled, but if you're still interested you can try to understand Gowers' proofs for when we actually start on it.

#### Mauricio Collares (Jun 23 2021 at 01:12):

Great! Thanks for letting me know and sorry for taking so long to reply. I was super busy (my deadline got extended by a few days) but now I have more free time. I will study Gowers' proof, hopefully I'll be able to help :)

#### Yaël Dillies (Jul 10 2021 at 07:29):

We have a bunch of constructions on simple_graph like

def is_uniform (ε : ℝ) (U W : finset α) : Prop :=
∀ U', U' ⊆ U → ∀ W', W' ⊆ W → ε * U.card ≤ U'.card → ε * W.card ≤ W'.card →
abs (edge_density G U' W' - edge_density G U W) < ε


Do you want me to PR them?

#### Kyle Miller (Jul 10 2021 at 20:06):

Yaël Dillies said:

Do you want me to PR them?

I think a good rule of thumb is that if formalized definitions have been tested by (partially) formalizing something else, then yes! I assume you have some sense of whether this works well for your application.

#### Bhavik Mehta (Jul 10 2021 at 20:09):

I think this definition is somewhat special to Szemeredi's regularity lemma and quasi-random properties of graphs, so probably should go in a new file (which probably will eventually contain the proof of SRL)

Last updated: Dec 20 2023 at 11:08 UTC