Ben Green's Open Problem 72

formal-conjectures · greens-open-problems · ams-5 · ams-52

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/\sqrt3 \approx 1.814$. Both are below $2$, so the expected answer to
the question above is yes.

The **no-k-in-line problem**:
For $N \geq k$ and $k > 2$, the AllowedSetSize is $(k - 1) N$, i. e. on an $N \times N$ subset,
there is a set of $(k - 1) N$ points for which no $k$ lie on a line (and not such a set of bigger size).

Note the range. [GK2025] proves this for $k > 10^{37}$, which is no_k_in_line_big below. At
$k = 3$ it is the claim Green expects to fail for large $N$, so this statement is not a
conjecture anyone has made across the whole range $k > 2$.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.72
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://en.wikipedia.org/wiki/No-three-in-line_problem
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/2510.17743
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/GreensOpenProblems/72.lean
Local target: Corpus.Green72.NoKInLine
Source SHA-256: bc44a880b841f79d83b664422853271551455c2b5b008090929fd4229ca5963b
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record