Szemerédi's theorem

szemeredi

Submitter: Kim Morrison.

Notes: §37 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (first additional statement of the section, generalizing Roth's theorem from 3-APs to k-APs). Every subset of ℕ of positive upper density contains arbitrarily long arithmetic progressions. Mathlib has Roth's theorem (roth_3ap_theorem_nat, the k = 3 case) but not the full Szemerédi theorem. As of 2026 it has not been formalized in any major proof assistant (a well-known open formalization target).

Source: E. Szemerédi, On sets of integers containing no k elements in arithmetic progression, Acta Arith. 27 (1975), 199-245. Listed as §37 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Szemerédi's original combinatorial proof relies on the Szemerédi regularity lemma plus a delicate density-increment argument. Furstenberg gave a measure-theoretic proof via multiple recurrence in ergodic theory (every measure-preserving system has the Multiple Recurrence Property for k commuting transformations). Gowers gave a Fourier-analytic proof introducing the Gowers uniformity norms U^k. Any of these formalisations is a major undertaking; all three structures (regularity, ergodic multiple recurrence, U^k norms) are absent from mathlib.

theorem declaration uses `sorry`szemeredi (A : Set ℕ) (h : 0 < upperDensity A) :
    LeanEval.Combinatorics.ContainsArbitraryAPs A := byA:Set ℕh:0 < upperDensity A⊢ ContainsArbitraryAPs A
  sorryAll goals completed! 🐙

Solved by

Not yet solved.