Email Gateway (Nov 16 2022 at 15:24): Email Gateway (Nov 16 2022 at 15:24):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I'd like to announce a new AFP entry.
Enjoy,
René
The Balog–Szemerédi–Gowers Theorem
by Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds
We formalise the Balog–Szemeré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édi's Theorem. 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.
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
Mathematics Tripos taught at the University of Cambridge. 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 . 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édi–Gowers Theorem
in any proof assistant to our knowledge.
https://www.isa-afp.org/entries/Balog_Szemeredi_Gowers.html
Last updated: Apr 19 2024 at 16:20 UTC