Roth's Theorem on Arithmetic Progressions (Q7361303)

We formalise a proof of Roth's Theorem on Arithmetic Progressions, a major result in additive combinatorics on the existence of 3-term arithmetic progressions in subsets of natural numbers. To this end, we follow a proof using graph regularity. We employ our recent formalisation of Szemerédi's Regularity Lemma, a major result in extremal graph theory, which we use here to prove the Triangle Counting Lemma and the Triangle Removal Lemma. Our sources are Yufei Zhao's MIT lecture notes " Graph Theory and Additive Combinatorics " (latest version here ) and W.T. Gowers's Cambridge lecture notes " Topics in Combinatorics ". We also refer to the University of Georgia notes by Stephanie Bell and Will Grodzicki, " Using Szemerédi's Regularity Lemma to Prove Roth's Theorem ".