Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC