72.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 5 contain sorry, 0 declared as axioms

Ben 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:

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

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Wikipedia/NoThreeInLineProblem.lean

structure Green72.AllowedSet We say a subset of $[N]^2$ is allowed for some $k$ if it contains no $k$ points which lie on a common line line 49 source
Source documentation
We say a subset of $[N]^2$ is allowed for some $k$ if it contains no $k$ points which lie on a common line.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
```
structure AllowedSet (k : ℕ) (N : ℕ) (s : Finset (ℕ × ℕ)) : Prop where
…
```
def Green72.AllowedSetSize The maximal size of an allowed set line 55 source
Source documentation
The maximal size of an allowed set

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, Prod, And, Eq, Finset.card, Green72.AllowedSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def AllowedSetSize (k : ℕ) (N : ℕ) : ℕ :=
…
```
theorem Green72.allowedSetSize_le 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$ line 61 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Green72.AllowedSetSize, HMul.hMul, HSub.hSub, OfNat.ofNat
Proof uses: csSup_le', Set.ofPred, Exists, Finset, Prod, And, Eq, Finset.card, Green72.AllowedSet, Membership.mem, Set, Finset.range, Finset.filter, Prod.fst, Decidable.byContradiction, Not, False, Finset.exists_subset_card_eq, Green72.AllowedSet.not_collinear, LE.le.trans and 40 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem allowedSetSize_le {k : ℕ} {N : ℕ} :
    AllowedSetSize k N ≤ (k - 1) * N := by
…
```
Mentions: Green72.AllowedSetSize
def Green72.NoKInLineFor The proposition that the allowed-set size for $k$ and $N$ is $(k - 1) * N$ line 84 source
Source documentation
The proposition that the allowed-set size for $k$ and $N$ is $(k - 1) * N$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Eq, Green72.AllowedSetSize, HMul.hMul, HSub.hSub, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def NoKInLineFor (k : ℕ) (N : ℕ) : Prop :=
…
```
theorem Green72.NoKInLine Documented declaration: NoKInLine sorry line 96 source
Source documentation
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.

depends on sorry what this means
Statement uses: Eq, Set, Nat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Set.ofPred, And, LT.lt, LE.le, Green72.NoKInLineFor
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem NoKInLine : answer(sorry) = {k | 2 < k ∧ ∀ N, k ≤ N → NoKInLineFor k N} := by
…
```
Mentions: Green72.NoKInLineFor
theorem Green72.green_72 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? sorry line 103 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, Filter.Eventually, Nat, Not, Green72.NoKInLineFor, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_72 : answer(sorry) ↔ ∀ᶠ N in Filter.atTop, ¬ NoKInLineFor 3 N := by
…
```
Mentions: Green72.NoKInLineFor
theorem Green72.green_72.variants.eventually Is $2N$ attained for all sufficiently large $N$? sorry line 114 source
Source documentation
Is $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.

depends on sorry what this means
Statement uses: Iff, True, Filter.Eventually, Nat, Green72.NoKInLineFor, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_72.variants.eventually : answer(sorry) ↔ ∀ᶠ N in Filter.atTop, NoKInLineFor 3 N := by
…
```
Mentions: Green72.NoKInLineFor
theorem Green72.no_three_in_line_le For $N \leq 60$, this has been verified with computers sorry line 119 source
Source documentation
For $N \leq 60$, this has been verified with computers.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Green72.NoKInLineFor
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem no_three_in_line_le {N : ℕ} (hN : 3 ≤ N) (hN' : N ≤ 60) :
    NoKInLineFor 3 N := by
…
```
Mentions: Green72.NoKInLineFor
theorem Green72.no_k_in_line_big In [GK2025] Grebennikov and Kwan prove that the pigeonhole bound $(k - 1) N$ is attained for $k > 10 ^ {37}$ and $N \geq k$ sorry line 126 source
Source documentation
In [GK2025] Grebennikov and Kwan prove that the pigeonhole bound $(k - 1) N$ is attained for $k > 10 ^ {37}$ and $N \geq k$.

depends on sorry what this means
Statement uses: Nat, LT.lt, HPow.hPow, OfNat.ofNat, LE.le, Green72.NoKInLineFor
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem no_k_in_line_big {k : ℕ} (N : ℕ) (h : 10 ^ 37 < k) (hN : k ≤ N) :
    NoKInLineFor k N := by
…
```
Mentions: Green72.NoKInLineFor