Định lý Szemerédi (dạng hữu hạn)

Bước 1 (quy về cửa sổ hữu hạn). Giả sử phát biểu vô hạn sai với một $d(A_0) > 0$ nào đó mà hoàn toàn không chứa cấp số cộng độ dài $k$. Khi đó với mọi $N$, phần hạn chế $A_0 \cap [1,N]$ là tập con không chứa cấp số cộng độ dài $k$ của $\{1,\dots,N\}$ có kích thước tăng như $\delta$$N$ với $\delta$ > 0 cố định. Nếu phát biểu hữu hạn đúng thì không thể có họ như vậy với $N$ lớn tùy ý — mâu thuẫn, nên hai phát biểu tương đương với nhau.

Bước 2 (phân hoạch chính quy). Xem mỗi cấp số cộng độ dài $k$ tiềm năng trong $\{1,\dots,N\}$ như một cạnh của siêu đồ thị $(k-1)$-đều. Bổ đề chính quy hóa siêu đồ thị chia tập đỉnh thành số phần bị chặn sao cho, trừ một phần ngoại lệ nhỏ, mọi bộ phần đều giống ngẫu nhiên: mật độ cạnh giữa chúng gần như hằng số, không có cụm con đậm đặc hay thưa bất thường.

Bước 3 (bổ đề đếm). Khi phân hoạch đã chính quy, một bổ đề đếm tương ứng cho thấy mọi bộ phần có mật độ tương đối dương phải chứa đúng số lượng cấu hình đầy đủ như kỳ vọng — đặc biệt, ít nhất một cấp số cộng độ dài $k$ thực sự tồn tại, vì cấu trúc chính quy giống ngẫu nhiên có mật độ dương không thể tránh được mẫu hình mà nó đang được kiểm tra.

Bước 4 (lập luận loại bỏ). Nếu $A$ hoàn toàn không có cấp số cộng độ dài $k$, bổ đề đếm sẽ buộc hầu hết cấu hình được đếm bởi phân hoạch chính quy trở nên suy biến, từ đó có thể xóa một số phần tử nhỏ không đáng kể khỏi $A$ để triệt tiêu mọi cấp số cộng gần đúng — mâu thuẫn với việc $A$ giữ mật độ $\delta$ trên tập kích thước $N$ lớn tùy ý. Vậy cấp số cộng độ dài $k$ phải tồn tại. (Chứng minh bằng lý thuyết ergodic của Furstenberg năm 1977 và chứng minh bằng giải tích Fourier bậc cao của Gowers đi đến cùng kết luận theo những con đường hoàn toàn khác nhau, mỗi cách đều cho cận tường minh nhưng cực lớn cho $N(k,\delta)$.)