Proved, in the site's label (PROVED (LEAN)); the suffix is a catalog label explained under Formalization. The question is answered yes: without a bound, the answer is a consequence of Furstenberg and Katznelson's density Hales–Jewett theorem (J. Analyse Math. 57 (1991), 64--119, refereed), and Solymosi (Combin. Probab. Comput. 13 (2004), 263--267, refereed) gives a quantitative proof whose bound on the threshold $N_0(\delta)$ is, because of the regularity lemma, at best of tower type; both prove Graham's axis-parallel form, which implies the form allowing any square. The claim pages are Furstenberg–Katznelson and Solymosi, both accepted on the refereed publications and the site's credit; the 2026 Lean formalization of Solymosi's paper is linked on his page (not built by this corpus, so it gives no formalized evidence).