License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.9
URN: urn:nbn:de:0030-drops-167185
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16718/
Dillies, Yaël ;
Mehta, Bhavik
Formalising Szemerédi’s Regularity Lemma in Lean
Abstract
Szemerédi’s Regularity Lemma is a fundamental result in graph theory with extensive applications to combinatorics and number theory. In essence, it says that all graphs can be approximated by well-behaved unions of random bipartite graphs. We present a formalisation in the Lean theorem prover of a strong version of this lemma in which each part of the union must be approximately the same size. This stronger version has not been formalised previously in any theorem prover. Our proof closely follows the pen-and-paper method, allowing our formalisation to provide an explicit upper bound on the number of parts. An application of this lemma is also formalised, namely Roth’s theorem on arithmetic progressions in qualitative form via the triangle removal lemma.
BibTeX - Entry
@InProceedings{dillies_et_al:LIPIcs.ITP.2022.9,
author = {Dillies, Ya\"{e}l and Mehta, Bhavik},
title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16718},
URN = {urn:nbn:de:0030-drops-167185},
doi = {10.4230/LIPIcs.ITP.2022.9},
annote = {Keywords: Lean, formalisation, formal proof, graph theory, combinatorics, additive combinatorics, Szemer\'{e}di’s Regularity Lemma, Roth’s Theorem}
}
