Szemerédi's theorem (finitary form)

Step 1 (reduction to the finite window). Suppose the infinite statement fails for some $d(A_0) > 0$ with no length-$k$ progression at all. Then for every $N$, the restriction $A_0 \cap [1,N]$ is a length-$k$-AP-free subset of $\{1,\dots,N\}$ whose size grows like $\delta$$N$ for a fixed $\delta$ > 0. If the finitary statement were true, no such family could exist for arbitrarily large $N$, a contradiction — so the two statements stand or fall together.

Step 2 (regularity partition). View potential $k$-term progressions in $\{1,\dots,N\}$ as edges of a $(k-1)$-uniform hypergraph. The hypergraph regularity lemma partitions the underlying vertex set into a bounded number of pieces so that, apart from a small exceptional fraction, every tuple of pieces is pseudorandom: the density of hyperedges between them is essentially constant, with no denser or sparser sub-clusters.

Step 3 (counting lemma). Once the partition is regular, a matching counting lemma shows that any tuple of pieces with positive relative density must contain the expected number of complete configurations — in particular, at least one genuine length-$k$ progression, because a regular pseudorandom structure with positive density cannot avoid the pattern it is being tested against.

Step 4 (removal argument). If $A$ had no length-$k$ progression at all, the counting lemma would force almost all of the configurations counted by the regular partition to be degenerate, which in turn would let one delete a vanishingly small number of elements from $A$ to kill every approximate progression — contradicting that $A$ keeps density $\delta$ on a set of size $N$ as large as we like. Hence a length-$k$ progression must exist. (Furstenberg's 1977 ergodic-theoretic proof and Gowers' higher-order Fourier-analytic proof reach the same conclusion by entirely different routes, each yielding explicit but astronomically large bounds on $N(k,\delta)$.)