Isabelle/HOL

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
Cite DOI URL