University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers  > Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL

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 Koutsoukou-Argyraki.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2023 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity