Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 185

claims/: The 2 claim pages of Problem 185, one per claimant's result; the problem's standing derives from them.

Statement. 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)$ ?

Status. 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), 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), 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).

Source. erdosproblems.com/185, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #185, https://www.erdosproblems.com/185.

References.

[FuKa91] Furstenberg, H. and Katznelson, Y., A density version of the Hales-Jewett Theorem. Journal d'Analyse Mathématique 57 (1991), 64-119.

Formalization. Statement in formal-conjectures, which at its commit of 2026-10-06 is tagged solved and names as the formal proof the file src/latest/ErdosProblems/Erdos185.lean of Boris Alexeev's lean-proofs repository (added 2026-08-17, last changed 2026-08-23; pinned at the commit of 2026-09-15 on the Dodos--Kanellopoulos--Tyros claim page as a formalization of the ternary density Hales--Jewett theorem by their argument and its application to Moser sets, with Codex and GPT-5.6 Sol as its formal authors). The community database (teorth/erdosproblems) lists status "proved (Lean)", formal_status Lean and formalized "yes", as of its entry's last update of 2026-08-24; it does not date the state changes. This corpus has not built or checked the development, and no local kernel credit is claimed.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (7)

Density Hales-Jewett theorem settles Moser's cube problem Dodos, Kanellopoulos and Tyros's density Hales-Jewett proof applied to Moser sets problems/additive_combinatorics/E0185/claims Sumsets and Arithmetic Progressions additive_combinatorics/polymath_2012_new_proof_density_halesjewett_theorem Theorem 1.4 (p. 2): the density Hales-Jewett theorem, every subset of [k]^n of density at least delta contains a combinatorial line once n >= DHJ(k, delta)Theorem 1.5 (p. 3): DHJ_3(delta) may be taken to be a tower of 2s of height O(1/delta^2); for k >= 4 the bound is broadly comparable to A_k(1/delta)

Graph