/-
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.
Given $N > 2$ and more than $2 * N$ points on an $N \times N$-grid, are there $3$ of the points on a common line?
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).
@[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: The no-k-in-line conjecture holds for $k = 3$.
@[category research open, AMS 5 52]
theorem green_72 {N : ℕ} (hN : 3 ≤ N) : NoKInLineFor 3 N := N:ℕhN:3 ≤ N⊢ NoKInLineFor 3 N
All goals completed! 🐙alias no_three_in_line := green_72Does the no-three-in-line problem hold when $N$ is big enough?
@[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