Abstract
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.