Ben Green's Open Problem 72

The question

NoKInLine. The no-k-in-line problem: For which $k>2$ does every $N\times N$ grid with $N\ge k$ contain a set of $(k-1)N$ points with no $k$ on a line, so that AllowedSetSize k N is the pigeonhole bound $(k-1)N$?

[GK2025] proves that every $k>10^{37}$ has this property, which is no_k_in_line_big below, and does not optimise this constant. At $k=3$ it is the property that Green expects to fail for large $N$, see green_72.

green_72. Green's Open Problem 72 / No-three-in-line problem: For $N$ sufficiently large, is it impossible to have $2N$ points in $[N{]}^2$ with no three in a line? Green suspects the answer is yes, and that $(3/2+o(1))N$ is optimal.

More commonly known as the no-three-in-line problem.

What is the largest subset of the grid $[N{]}^2$ with no three points in a line? In particular, for $N$ sufficiently large, is it impossible to have a set of size $2N$ with this property?

The upper bound $2N$ is the easy half and is allowedSetSize_le below, by pigeonhole on the columns. The open content is whether $2N$ is attained. Green records that it is for $N$ up to around 50, that $(3/2+o(1))N$ points are achievable for arbitrary $N$, and that his "personal suspicion is that this is optimal". The Wikipedia reference points the same way: Guy and Kelly conjectured $c=\sqrt[3]{2{\pi }^2/3}\approx 1.874$, and after an error in the heuristic was found Guy corrected it to $c=\pi /\sqrt{3}\approx 1.814$. Both are below $2$, so the expected answer to the question above is yes.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.GreensOpenProblems.«72» (2 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem NoKInLine : answer(sorry) = {k | 2 < k ∧ ∀ N, k ≤ N → NoKInLineFor k N}

theorem green_72 : answer(sorry) ↔ ∀ᶠ N in Filter.atTop, ¬ NoKInLineFor 3 N

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

• green_72.variants.eventually — Is 2N attained for all sufficiently large N? This is not the negation of green_72.

References

• Ben Green's Open Problem 72
• Wikipedia
• [GK2025] Grebennikov, A. Kwan, M. No $(k+1)$-in-line problem for large constant $k$. https://arxiv.org/abs/2510.17743

Source and licence

Imported from Formal Conjectures (Ben Green's 100 open problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.