Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL

Add to your list(s) Download to your calendar using vCal

• Mantas Bakšys (University of Cambridge)
• Thursday 23 February 2023, 17:00-18:00
• Centre for Mathematical Sciences MR12, CMS.

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.

This talk is included in these lists:

• Centre for Mathematical Sciences MR12, CMS
• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.