### Abstract

We formalise a proof of Roth's Theorem on Arithmetic Progressions, a major result in additive combinatorics on the existence of 3-term arithmetic progressions in subsets of natural numbers. To this end, we follow a proof using graph regularity. We employ our recent formalisation of Szemerédi's Regularity Lemma, a major result in extremal graph theory, which we use here to prove the Triangle Counting Lemma and the Triangle Removal Lemma. Our sources are Yufei Zhao's MIT lecture notes "Graph Theory and Additive Combinatorics" (latest version here) and W.T. Gowers's Cambridge lecture notes "Topics in Combinatorics". We also refer to the University of Georgia notes by Stephanie Bell and Will Grodzicki, "Using Szemerédi's Regularity Lemma to Prove Roth's Theorem".

### License

BSD License

### Topics

- Mathematics/Graph theory
- Mathematics/Combinatorics

### Session Roth_Arithmetic_Progressions

- Roth_Arithmetic_Progressions

### Depends on

- Ergodic Theory
- A Probabilistic Proof of the Girth-Chromatic Number Theorem
- Properties of Random Graphs – Subgraph Containment
- Szemerédi’s Regularity Lemma

### Auto-related entries

- Turán’s Graph Theorem

## Cite

×

Roth_Arithmetic_Progressions-AFP

    @article{Roth_Arithmetic_Progressions-AFP,
      author  = {Chelsea Edmonds and Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson},
      title   = {Roth's Theorem on Arithmetic Progressions},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Roth_Arithmetic_Progressions.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jan 3, 2022 : Isabelle2021-1