Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Szemerédi's theorem

Conjectura.Statements.Mathematics.Combinatorics.SzemerediTheorem

/-
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
-/
import Conjectura.Defs.Mathematics.Combinatorics.UpperDensity
import Conjectura.Defs.Mathematics.Combinatorics.ArithmeticProgression

/-! # Szemerédi's theorem -/

namespace Conjectura.Combinatorics

/-- **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

end Conjectura.Combinatorics