Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Angeliki KoutsoukouArgyraki.
The Balog–Szemerédi–Gowers Theorem is 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 involves an interplay of different mathematical areas, namely applications of graph theory and probability theory to additive combinatorics. With our successful formalisation, we demonstrate how locales, Isabelle’s module system, can be employed to handle such complex interplays in the formalisation of mathematics.
This talk is part of the Formalisation of mathematics with interactive theorem provers series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
