Szemerédi's Regularity Lemma

Chelsea Edmonds 🌐, Angeliki Koutsoukou-Argyraki 🌐 and Lawrence C. Paulson 🌐

November 5, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Szemerédi's regularity lemma is a key result in the study of large graphs. It asserts the existence of an upper bound on the number of parts the vertices of a graph need to be partitioned into such that the edges between the parts are random in a certain sense. This bound depends only on the desired precision and not on the graph itself, in the spirit of Ramsey's theorem. The formalisation follows online course notes by Tim Gowers and Yufei Zhao.


BSD License


Session Szemeredi_Regularity