/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilBen Green's Open Problem 72
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.
References:
[GK2025] Grebennikov, A. Kwan, M. No $(k + 1)$-in-line problem for large constant $k$. https://arxiv.org/abs/2510.17743
namespace Green72We say a subset of $[N]^2$ is allowed for some $k$ if it contains no $k$ points which lie on a common line.
structure AllowedSet (k : ℕ) (N : ℕ) (s : Finset (ℕ × ℕ)) : Prop where
is_bounded : ∀ i ∈ s, i.1 < N ∧ i.2 < N
not_collinear : ∀ ⦃t : Finset (ℕ × ℕ)⦄, t ⊆ s → t.card = k →
¬ Collinear ℝ ({r | ∃ i ∈ t, r = ((↑i.1 : ℝ), (↑i.2 : ℝ))} : Set (ℝ × ℝ))The maximal size of an allowed set
noncomputable def AllowedSetSize (k : ℕ) (N : ℕ) : ℕ :=
sSup {r | ∃ s, r = s.card ∧ AllowedSet k N s}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$.
k:ℕN:ℕs:Finset (ℕ × ℕ)hs:AllowedSet k N skey:∀ x ∈ Finset.range N, {i ∈ s | i.1 = x}.card ≤ k - 1⊢ s.card ≤ (k - 1) * N
calc s.card
= ∑ x ∈ Finset.range N, (s.filter fun i => i.1 = x).card :=
Finset.card_eq_sum_card_fiberwise fun i hi => Finset.mem_range.mpr (hs.is_bounded i hi).1
_ ≤ ∑ _x ∈ Finset.range N, (k - 1) := Finset.sum_le_sum key
_ = (k - 1) * N := k:ℕN:ℕs:Finset (ℕ × ℕ)hs:AllowedSet k N skey:∀ x ∈ Finset.range N, {i ∈ s | i.1 = x}.card ≤ k - 1⊢ ∑ _x ∈ Finset.range N, (k - 1) = (k - 1) * N All goals completed! 🐙The proposition that the allowed-set size for $k$ and $N$ is $(k - 1) * N$.
def NoKInLineFor (k : ℕ) (N : ℕ) : Prop :=
AllowedSetSize k N = (k - 1) * NThe 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$.
@[category research open, AMS 5 52]
theorem NoKInLine {k : ℕ} {N : ℕ} (hk : 2 < k) (h : k ≤ N) : NoKInLineFor k N := k:ℕN:ℕhk:2 < kh:k ≤ N⊢ NoKInLineFor k N
All goals completed! 🐙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.
@[category research open, AMS 5 52]
theorem green_72 : answer(sorry) ↔ ∀ᶠ N in Filter.atTop, ¬ NoKInLineFor 3 N := ⊢ True ↔ ∀ᶠ (N : ℕ) in Filter.atTop, ¬NoKInLineFor 3 N
All goals completed! 🐙alias no_three_in_line := green_72Is $2N$ attained for all sufficiently large $N$?
This is not the negation of green_72. Negating that one gives $\exists^f N$ where this asks
$\forall^f N$, so both can be answered False if the behaviour oscillates. Green asks his
question in the green_72 form.
@[category research open, AMS 5 52]
theorem green_72.variants.eventually : answer(sorry) ↔ ∀ᶠ N in Filter.atTop, NoKInLineFor 3 N := ⊢ True ↔ ∀ᶠ (N : ℕ) in Filter.atTop, NoKInLineFor 3 N
All goals completed! 🐙For $N \leq 60$, this has been verified with computers.
@[category research solved, AMS 5 52]
theorem no_three_in_line_le {N : ℕ} (hN : 3 ≤ N) (hN' : N ≤ 60) :
NoKInLineFor 3 N := N:ℕhN:3 ≤ NhN':N ≤ 60⊢ NoKInLineFor 3 N
All goals completed! 🐙In [GK2025] Grebennikov and Kwan prove the no-k-in-line conjecture for $k > 10 ^ 37$ and $N \geq k$.
@[category research solved, AMS 5 52]
theorem no_k_in_line_big {k : ℕ} (N : ℕ) (h : 10 ^ 37 < k) (hN : k ≤ N) :
NoKInLineFor k N := k:ℕN:ℕh:10 ^ 37 < khN:k ≤ N⊢ NoKInLineFor k N
All goals completed! 🐙-- TODO: Add lower bound for no-three-in-line
end Green72