Formalising Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL

TL;DR

This paper presents a formalisation of Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions within Isabelle/HOL, demonstrating the use of proof assistants in formalising complex combinatorial results.

Contribution

It introduces the first formalisation of these fundamental theorems in Isabelle/HOL, including key lemmas like the Triangle Counting and Triangle Removal Lemmas.

Findings

Successful formalisation of Szemerédi's Regularity Lemma

Formal proof of Roth's Theorem on Arithmetic Progressions

Identification of challenges and solutions in formalising combinatorial proofs

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.