PROVED (LEAN): the site's label. The answer is yes, a corollary of the density Hales--Jewett theorem of Furstenberg and Katznelson, since the three points of a combinatorial line in $\{0,1,2\}^n$ are collinear (claim page (Furstenberg and Katznelson, 1991)), accepted on the theorem's refereed publication and the site's adoption, and through the shorter proof of the theorem by Dodos, Kanellopoulos and Tyros (claim page (Dodos, Kanellopoulos and Tyros, 2012)), accepted on its refereed publication alone; neither rests 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 problem through the Dodos--Kanellopoulos--Tyros argument, linked on their claim page; this corpus has not built or audited it, so no claim lists formalized evidence (see Formalization).