  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.
