### Abstract

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"
(revised 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".

BSD License