Szemerédi's theorem

szemeredi — a formalization challenge from the lean-eval benchmark.

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).

Formal statement

/-- **Szemerédi's theorem.** Every subset of `ℕ` of positive upper density
contains arbitrarily long arithmetic progressions. -/
theorem szemeredi (A : Set ℕ) (h : 0 < upperDensity A) :
    ContainsArbitraryAPs A := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: szemeredi
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.