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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

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

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Yusuf Hamied Theatre, Christ's College Hybrid: in-person in Cambridge & online via Teams Collaboration Skills Initiative

Other talks

Understanding the Interplay between LLMs' Utilisation of Parametric and Contextual Knowledge The Magic of Magnetism Morning Break Talk TBC Tea and Coffee Break Welcome Reception and Poster Session
 

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