The board / additive combinatorics / #171
Erdős Problem #171
density Hales-Jewett
PROVED LEANdatabase updated 2026-08-24
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Is it true that for every \(\epsilon>0\) and integer \(t\geq 1\), if \(N\) is sufficiently large and \(A\) is a subset of \([t]^N\) of size at least \(\epsilon t^N\) then \(A\) must contain a combinatorial line \(P\) (a set \(P=\{p_1,\ldots,p_t\}\) where for each coordinate \(1\leq j\leq t\) the \(j\)th coordinate of \(p_i\) is either \(i\) or constant). The 'density Hales-Jewett' problem. This was proved by Furstenberg and Katznelson [FuKa91]. A new elementary proof, which gives quantitative bounds, was proved by the Polymath project [Po12]. Combinatorial lines are Mathlib's `Combinatorics.Line (Fin t) (Fin N)` (which have at least one non-constant coordinate).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/171.Prizenone
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA156989
Original pageerdosproblems.com/171
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.