BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabel
 le/HOL - Mantas Bakšys (University of Cambridge)
DTSTART:20230223T170000Z
DTEND:20230223T180000Z
UID:TALK193399@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:The Balog–Szemerédi–Gowers Theorem is a profound result i
 n additive combinatorics which played a central role in Gowers’s proof d
 eriving the first effective bounds for Szemerédi’s Theorem. The proof i
 nvolves an interplay of different mathematical areas\, namely applications
  of graph theory and probability theory to additive combinatorics. With ou
 r successful formalisation\, we demonstrate how locales\, Isabelle’s mod
 ule system\, can be employed to handle such complex interplays in the form
 alisation of mathematics.
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR