Szemerédi's Theorem

Another well known result of Ramsey theory is Van der Waerden's theorem:

If $\mathbb{N}$ is colored with finitely many colors, then one of the colors contains arithmetic progressions of arbitrary finite length.

Using a method of Shelah, Van der Waerden's theorem is known to be provable in $\mathsf{RCA}_0$. The so-called ``density version'' of Van der Waerden's theorem is due to Szemerédi:

If $A\subseteq\mathbb{N}$ is such that

$$\limsup_{n\to\infty}\frac{\vert A\cap\{1,\dots,n\}\vert}n>0$$

then A contains arithmetic progressions of arbitrary finite length.

Essentially nothing is known about the strength of Szemerédi's theorem. In particular it is unknown whether Szemerédi's theorem is provable in $\mathsf{ACA}_0$.