Formalising Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
Logic in Computer Science
2022-10-14 v3
Abstract
We have formalised Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
Keywords
Cite
@article{arxiv.2207.07499,
title = {Formalising Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL},
author = {Chelsea Edmonds and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:2207.07499},
year = {2022}
}