Repository logo
 

Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL

Published version
Peer-reviewed

Change log

Abstract

jats:titleAbstract</jats:title>jats:pWe have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.</jats:p>

Description

Keywords

Interactive theorem proving, Proof assistant, Formalisation of mathematics, Isabelle, HOL, Additive combinatorics, Extremal graph theory, Arithmetic progressions, Number theory

Journal Title

Journal of Automated Reasoning

Conference Name

Journal ISSN

0168-7433
1573-0670

Volume Title

Publisher

Springer Science and Business Media LLC
Sponsorship
European Research Council (742178)