Search Results

Documents authored by Mehta, Bhavik


Document
Formalising Szemerédi’s Regularity Lemma in Lean

Authors: Yaël Dillies and Bhavik Mehta

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


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.

Cite as

Yaël Dillies and Bhavik Mehta. Formalising Szemerédi’s Regularity Lemma in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2022.9},
  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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail