Szemerédi's theorem

SzemerediPropdef

Szemerédi's theorem: any set of naturals of positive upperDensity contains arithmetic progressions of every finite length. Proved in 1975; the statement is kept here because a great many open questions are quantitative refinements of it.

def SzemerediProp : Prop :=
  ∀ S : Set ℕ, 0 < upperDensity S → ∀ k : ℕ, ContainsAPOfLength S k

Builds on

Upper density
Arithmetic progression

import Conjectura.Statements.Mathematics.Combinatorics.SzemerediTheorem · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits