A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
summary
The project formalises the Balog–Szemerédi–Gowers theorem in Isabelle/HOL, delivering the first proof assistant formalisation of that result, including a difference‑set statement and an alternate sumset version requiring a triangle inequality. It builds a new undirected graph library expressed with locales, encodes probabilistic dependent‑random‑selection via explicit probability‑space locales, proves many cardinality and projection lemmas that papers skip, and completes the development (three contributors, under two months) successfully with AFP entries and a paper.
AI-written summary · about
chapters (17)
- 0:00Formalization project intro
- 1:04What is additive combinatorics
- 2:07Formalizing BSGL theorem
- 3:10Key contributions and libraries
- 4:13Graph theory formalization challenges
- 5:57Locales in formalization
- 7:42Main theorem statement
- 8:23Proof structure overview
- 9:04Lemma 3.1 and random selection
- 10:50Lemma 3.2 and bipartite graphs
- 11:54Multiple locale instances
- 13:20Lemma 3.6 and graph construction
- 14:43Proof formalization challenges
- 15:46Main theorem as corollary
- 16:28Summary of challenges
- 17:32Speed and accessibility
- 18:18Q&A