\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{amssymb}
\usepackage{isabelle,isabellesym}
\usepackage[english]{babel}  % for guillemots

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{The Balog--Szemer\'{e}di--Gowers Theorem}
\author{Angeliki Koutsoukou-Argyraki, Mantas Bak\v{s}ys, and Chelsea Edmonds\\
University of Cambridge\\
\texttt{\{ak2110, mb2412, cle47\}@cam.ac.uk}}

\maketitle

\begin{abstract}
We formalise the Balog--Szemer\'{e}di--Gowers Theorem,  a profound result in additive combinatorics  which played a central role in Gowers's  proof deriving the first effective bounds for Szemer\'{e}di's Theorem \cite{GowersnewSzemeredi}.
The proof is of great mathematical interest given that it involves an interplay between different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics involving algebraic objects.
This interplay is what made the process of the formalisation, for which we had to develop formalisations of new background material in the aforementioned areas, more rich and technically challenging.  We demonstrate how locales, Isabelle's module system, can be employed to handle such interplays.
To treat the graph-theoretic aspects of the
proof, we make use of a new, more general undirected graph theory library developed recently by Chelsea Edmonds, which is both flexible and extensible \cite{Undirected_Graph_Theory-AFP}.
For the formalisation we followed a proof presented in the 2022 lecture notes by Timothy
Gowers "Introduction to Additive Combinatorics"  for Part III of the Mathematical Tripos taught at the University of Cambridge \cite{Gowersnotes}.
 In addition to the main theorem, which, following our source, is formulated for difference sets, we
also give an alternative version for sumsets which required a formalisation of an auxiliary triangle inequality
following a proof by Yufei Zhao from his book "Graph Theory and Additive
Combinatorics" \cite{Zhaobook}.
We moreover formalise a few
additional results  in additive combinatorics that are not used in the proof of the main theorem.
This is the first formalisation of the Balog--Szemer\'{e}di--Gowers Theorem in any proof assistant to our knowledge.

\end{abstract}
\newpage
\tableofcontents

\subsection*{Acknowledgements}
Angeliki Koutsoukou-Argyraki is funded by the ERC Advanced Grant ALEXANDRIA (Project GA
742178) funded by the European Research Council and led by Lawrence C. Paulson
(University of Cambridge, Department of Computer Science and Technology).
Mantas Bak\v{s}ys received funding for his internship supervised by Koutsoukou-Argyraki by the
Cambridge Mathematics Placements (CMP) Programme and by the ALEXANDRIA Project.
Chelsea Edmonds is jointly funded by the Cambridge Trust
(Cambridge Australia Scholarship) and a Cambridge Department of Computer Science and Technology Premium Research
Studentship.
\newpage

% include generated text of all theories
\input{session}


\bibliographystyle{abbrv}
\bibliography{root}


\end{document}
