Ben Green's Open Problem 72

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

Given $N \lt 2$ and a more than $2 * N$ points on an $N \times N$-grid, are there $3$ of the points on a common line?

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

structure Green72.AllowedSet (k N : ℕ) (s : Finset (ℕ × ℕ)) : Prop

We say a subset of $[N]^2$ is allowed for some $k$ if it contains no $k$ points which lie on a common line.

• is_bounded (i : ℕ × ℕ) : i ∈ s → i.1 < N ∧ i.2 < N
• not_collinear ⦃t : Finset (ℕ × ℕ)⦄ : t ⊆ s → t.card = k → Collinear ℝ {r : ℝ × ℝ | ∃ i ∈ s, r = (↑i.1, ↑i.2)}

noncomputable def Green72.AllowedSetSize (k N : ℕ) : ℕ

The maximal size of an allowed set

Equations

• Green72.AllowedSetSize k N = sSup {r : ℕ | ∃ (s : Finset (ℕ × ℕ)), r = s.card ∧ Green72.AllowedSet N k s}

theorem Green72.allowedSetSize_le {k N : ℕ} (h : k ≤ N) : AllowedSetSize k N ≤ (k - 1) * N

By the pigeon hole principle, the size of a subset of an $N \times N$ grid such that no $k$ points lie on a line is bounded by $\leq (k - 1) * N$ for $N \geq k$.

def Green72.NoKInLineFor (k N : ℕ) : Prop

$N, k$ when the AllowedSetSize of $N$ for $k$ is $k * N$.

Equations

• Green72.NoKInLineFor k N = (Green72.AllowedSetSize k N = (k - 1) * N)

theorem Green72.NoKInLine {k N : ℕ} (hk : 1 < k) (h : k ≤ N) : NoKInLineFor k N

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

theorem Green72.green_72 {N : ℕ} (hN : 3 ≤ N) : NoKInLineFor 3 N

Green's Open Problem 72 / No-three-in-line problem: The no-k-in-line conjecture holds for $k = 3$.

theorem Green72.no_three_in_line {N : ℕ} (hN : 3 ≤ N) : NoKInLineFor 3 N

Alias of Green72.green_72.

---

Green's Open Problem 72 / No-three-in-line problem: The no-k-in-line conjecture holds for $k = 3$.

theorem Green72.green_72.variants.eventually : ∀ᶠ (N : ℕ) in Filter.atTop, NoKInLineFor 3 N

Does the no-three-in-line problem hold when $N$ is big enough?

theorem Green72.no_three_in_line_le {N : ℕ} (hN : 3 ≤ N) (hN' : N ≤ 60) : NoKInLineFor 3 N

For $N \leq 60$, this has been verfied with computers.

theorem Green72.no_k_in_line_big {k : ℕ} (N : ℕ) (h : 10 ^ 37 < k) : NoKInLineFor k N

In [GK2025] Grebennikov and Kwan prove the no-k-in-line conjecture for $k > 10 ^ 37$.