Document Open Access Logo

Formalising Szemerédi’s Regularity Lemma in Lean

Authors Yaël Dillies , Bhavik Mehta

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.9.pdf
  • Filesize: 0.73 MB
  • 19 pages

Document Identifiers

Author Details

Yaël Dillies
  • Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, UK
Bhavik Mehta
  • Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, UK

Funding

  • Mehta, Bhavik: Cantab Capital Institute for the Mathematics of Information

Acknowledgements

We want to thank Anne Baanen, Thomas Bloom, Kevin Buzzard, Timothy Gowers, Heather Macbeth, the mathlib maintainers and the anonymous reviewers for useful comments on previous versions of this paper. We are grateful to the mathlib community, whose work has been invaluable for the prerequisites of this project.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.ITP.2022.9

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
  • Mathematics of computing → Extremal graph theory
Keywords
  • Lean
  • formalisation
  • formal proof
  • graph theory
  • combinatorics
  • additive combinatorics
  • Szemerédi’s Regularity Lemma
  • Roth’s Theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Miklós Ajtai and Endre Szemerédi. Sets of lattice points that form no squares. Stud. Sci. Math. Hungar, 9(1975):9-11, 1974. Google Scholar
  2. Noga Alon. Problems and results in extremal combinatorics-III. Journal of Combinatorics, 7(2):233-256, 2016. Google Scholar
  3. Thomas F Bloom and Olof Sisask. Breaking the logarithmic barrier in Roth’s theorem on arithmetic progressions. arXiv preprint arXiv:2007.03528, 2020. Google Scholar
  4. Béla Bollobás. Modern graph theory, volume 184. Springer Science & Business Media, 1998. Google Scholar
  5. Ricky W Butler and Jon A Sjogren. A PVS graph theory library, volume 206923. National Aeronautics and Space Administration, Langley Research Center, 1998. Google Scholar
  6. C Chvatál, Vojtech Rödl, Endre Szemerédi, and W Tom Trotter Jr. The Ramsey number of a graph with bounded maximum degree. Journal of Combinatorial Theory, Series B, 34(3):239-243, 1983. Google Scholar
  7. Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.15.
  8. Christian Doczkal and Damien Pous. Graph theory in coq: Minors, treewidth, and isomorphisms. Journal of Automated Reasoning, 64(5):795-825, 2020. Google Scholar
  9. Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. Roth’s Theorem on Arithmetic Progressions. Archive of Formal Proofs, December 2021. , Formal proof development. URL: https://isa-afp.org/entries/Roth_Arithmetic_Progressions.html.
  10. Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. Szemerédi’s Regularity Lemma. Archive of Formal Proofs, November 2021. , Formal proof development. URL: https://isa-afp.org/entries/Szemeredi_Regularity.html.
  11. Paul Erdös and Arthur H Stone. On the structure of linear graphs. Bulletin of the American Mathematical Society, 52(12):1087-1091, 1946. Google Scholar
  12. Jacob Fox. A new proof of the graph removal lemma. Annals of Mathematics, pages 561-579, 2011. Google Scholar
  13. William Timothy Gowers. Lower bounds of tower type for Szemerédi’s uniformity lemma. Geometric & Functional Analysis GAFA, 7(2):322-337, 1997. Google Scholar
  14. William Timothy Gowers. Hypergraph regularity and the multidimensional Szemerédi theorem. Annals of Mathematics, pages 897-946, 2007. Google Scholar
  15. Ben Green and Terence Tao. The primes contain arbitrarily long arithmetic progressions. Annals of mathematics, pages 481-547, 2008. Google Scholar
  16. Ben Green and Julia Wolf. A note on Elkin’s improvement of Behrend’s construction. In Additive number theory, pages 141-144. Springer, 2010. Google Scholar
  17. Alena Gusakov, Bhavik Mehta, and Kyle A. Miller. Formalizing Hall’s Marriage Theorem in Lean, 2021. URL: http://arxiv.org/abs/2101.00127.
  18. Sebastian Koch. Unification of graphs and relations in mizar. Formalized Mathematics, 28(2):173-186, 2020. Google Scholar
  19. János Komlós. The blow-up lemma. Combinatorics, Probability and Computing, 8(1-2):161-176, 1999. Google Scholar
  20. János Komlós, Ali Shokoufandeh, Miklós Simonovits, and Endre Szemerédi. The regularity lemma and its applications in graph theory. In Summer school on theoretical aspects of computer science, pages 84-112. Springer, 2000. Google Scholar
  21. W. Mantel. Problem 28 (Solution by H. Gouwentak, W. Mantel, J. Teixeira de Mattes, F. Schuh and W. A. Wythoff). Wiskundige Opgaven, 10:60-61, 1907. Google Scholar
  22. The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  23. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-388. Springer, 2015. Google Scholar
  24. Brendan Nagle, Vojtěch Rödl, and Mathias Schacht. The counting lemma for regular k-uniform hypergraphs. Random Structures & Algorithms, 28(2):113-179, 2006. Google Scholar
  25. Lars Noschinski. A graph library for isabelle. Mathematics in Computer Science, 9(1):23-39, 2015. Google Scholar
  26. Vojtěch Rödl and Jozef Skokan. Regularity lemma for k-uniform hypergraphs. Random Structures & Algorithms, 25(1):1-42, 2004. Google Scholar
  27. Klaus F Roth. On certain sets of integers. J. London Math. Soc, 28(104-109):3, 1953. Google Scholar
  28. József Solymosi. Note on a generalization of Roth’s theorem. In Discrete and computational geometry, pages 825-827. Springer, 2003. Google Scholar
  29. Endre Szemerédi. Regular partitions of graphs. Technical report, Stanford Univ Calif Dept of Computer Science, 1975. Google Scholar
  30. Andrew Thomason. Pseudo-random graphs. In North-Holland Mathematics Studies, volume 144, pages 307-331. Elsevier, 1987. Google Scholar
  31. Paul Turán. On an extremal problem in graph theory. Mat. Fiz. Lapok, 48:436-452, 1941. Google Scholar
  32. Yufei Zhao. Graph Theory and Additive Combinatorics, 2019. URL: https://yufeizhao.com/gtac/gtac.pdf.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact