/-
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.
-/
module
public 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
@[expose] public sectionnamespace 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) * N
The no-k-in-line problem:
For which $k > 2$ does every $N \times N$ grid with $N \geq 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.
@[category research open, AMS 5 52]
theorem NoKInLine : answer(sorry) = {k | 2 < k ∧ ∀ N, k ≤ N → NoKInLineFor k N} := ⊢ sorry = {k | 2 < k ∧ ∀ (N : ℕ), 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 that the pigeonhole bound $(k - 1) N$ is attained 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