The board / additive combinatorics / #185
Erdős Problem #185
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).
\(f_3(n)\) is the maximal size of a subset of \(\{0,1,2\}^n\) which contains no three points on a line (in \(\mathbb{R}^n\)).
Let \(f_3(n)\) be the maximal size of a subset of \(\{0,1,2\}^n\) which contains no three points on a line. Is it true that \(f_3(n)=o(3^n)\)? Originally considered by Moser. It is trivial that \(f_3(n)\geq R_3(3^n)\), the maximal size of a subset of \(\{1,\ldots,3^n\}\) without a three-term arithmetic progression. Moser showed that \[f_3(n) \gg \frac{3^n}{\sqrt{n}}.\] The answer is yes, which is a corollary of the density Hales-Jewett theorem, proved by Furstenberg and Katznelson [FuKa91].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/185.Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA003142
Original pageerdosproblems.com/185
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.