PROVED (LEAN): the site's label. The answer is yes, by the density Hales--Jewett theorem of Furstenberg and Katznelson (claim page (Furstenberg and Katznelson, 1991)), reproved with explicit bounds by the Polymath project (claim page (Polymath, 2009)) and again, by a shorter density-increment argument, by Dodos, Kanellopoulos and Tyros (claim page (Dodos, Kanellopoulos and Tyros, 2012)); the first two claims are accepted on their refereed publication and the site's adoption, the third on its refereed publication alone, and none on any review by this project. The site's Lean marker traces to the community database's Lean record and to the Lean development in Boris Alexeev's lean-proofs repository that declares itself a formalization of the Dodos--Kanellopoulos--Tyros proof, linked on their claim page; this corpus has not built or audited it, so no claim lists formalized evidence (see Formalization).