interactive theorem proving

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

We describe our formalisation in the interactive theorem prover Isabelle/HOL of the Balog–Szemerédi–Gowers Theorem, a profound result …

Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds