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

### License

BSD License

### Topics

- Mathematics/Graph theory
- Mathematics/Combinatorics

### Session Szemeredi_Regularity

- Szemeredi

### Depends on

- A Probabilistic Proof of the Girth-Chromatic Number Theorem

### Used by

- Roth’s Theorem on Arithmetic Progressions

### Auto-related entries

- Roth’s Theorem on Arithmetic Progressions
- Pratt’s Primality Certificates

## Cite

×

Szemeredi_Regularity-AFP

    @article{Szemeredi_Regularity-AFP,
      author  = {Chelsea Edmonds and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
      title   = {Szemerédi's Regularity Lemma},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Szemeredi_Regularity.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 7, 2021 : Isabelle2021