---

Claim. For every $k$ and $\delta>0$ there is $\mathrm{DHJ}(k,\delta)$ such that every subset of $[k]^n$ of density at least $\delta$ contains a combinatorial line once $n\ge\mathrm{DHJ}(k,\delta)$ (Theorem 1.4 of the paper), and the bound is explicit: for $k=3$ a tower of twos of height $O(1/\delta^2)$, and for $k\ge4$ a bound of Ackermann type (Theorem 1.5 of the Annals version; equivalently, a subset of $[3]^n$ with no combinatorial line has density $O(1/\sqrt{\log^*n})$). D. H. J. Polymath, A new proof of the density Hales--Jewett theorem, Ann. of Math. (2) 175 (2012), no. 3, 1283--1327, arXiv:0910.3926 (v1 20 October 2009, v2 16 February 2010), cited as [Po12] on the problem page; library home polymath_2012_new_proof_density_halesjewett_theorem. With $k=t$ and $\delta=\epsilon$ this is the question of Problem 171, answered yes. The argument is a density-increment scheme carried out combinatorially, the first proof of the theorem that is elementary and the first that yields any bound; the original proof is Furstenberg and Katznelson's (claim page).

Depends on. No page of this wiki: the proof is self-contained and does not use the Furstenberg--Katznelson argument.

Acceptance. Refereed: the paper appeared in the Annals of Mathematics; the publication record dates the issue to 1 May 2012. Reviewed: the site's curator, Thomas Bloom, records it in the problem page's commentary as a second, elementary proof that also yields bounds (label PROVED (LEAN), page last edited 25 January 2026). The library card digests the paper; its proof was not reviewed by this project, and nothing here rests on such a review. The site's Lean marker traces to a formalization of the Dodos--Kanellopoulos--Tyros proof of the theorem, pinned on their claim page, not of this one, so no formalized evidence is listed.