872.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

14 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 872

This file states Erdős Problem 872 for the primitive-set saturation game on $\{2, \dots, n\}$. The game value L n is defined by a finite minimax recursion: Prolonger moves first and maximizes the final size of the claimed primitive set, while Shortener minimizes it.

The problem statement does not fix the turn order. This file fixes Prolonger to move first, following the convention used in the forum discussion of the problem. The choice is not cosmetic: computational data suggests the Shortener-first value tracks $\pi(n)$ while the Prolonger-first value grows linearly, and the questions below concern the Prolonger-first quantity.

References:

Imports (1)

FormalConjecturesUtil

def Erdos872.IsPrimitive A primitive subset of $\{2, \dots, n\}$ is a set in which no element divides another line 48 source
Source documentation
A primitive subset of $\{2, \dots, n\}$ is a set in which no element divides another. The quantified divisibility condition is one-sided because the variables range over all ordered pairs of distinct elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: And, LE.le, Finset.Icc, OfNat.ofNat, Membership.mem, Ne, Not, Dvd.dvd
9 instances, coercions and auxiliary constants left out.
```
def IsPrimitive (n : ℕ) (A : Finset ℕ) : Prop :=
…
```
structure Erdos872.GamePos A game position consists of the already claimed set and the still unclaimed pool line 62 source
Source documentation
A game position consists of the already claimed set and the still unclaimed pool.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat
```
structure GamePos (n : ℕ) where
…
```
def Erdos872.legalMoves The legal moves from a position: unclaimed elements whose insertion preserves primitiveness line 67 source
Source documentation
The legal moves from a position: unclaimed elements whose insertion preserves primitiveness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos872.GamePos, Finset
Proof uses: Finset.filter, Erdos872.IsPrimitive, Insert.insert, Erdos872.GamePos.claimed, Classical.propDecidable, Erdos872.GamePos.pool
2 instances, coercions and auxiliary constants left out.
```
def legalMoves {n : ℕ} (p : GamePos n) : Finset ℕ :=
…
```
Mentions: Erdos872.GamePos
lemma Erdos872.mem_legalMoves Membership in legalMoves: a legal move is a pool element whose insertion preserves primitiveness line 74 source
Source documentation
Membership in legalMoves: a legal move is a pool element whose insertion preserves primitiveness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos872.GamePos, Iff, Membership.mem, Finset, Erdos872.legalMoves, And, Erdos872.GamePos.pool, Erdos872.IsPrimitive, Insert.insert, Erdos872.GamePos.claimed
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Classical.propDecidable, iff_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_legalMoves {n : ℕ} {p : GamePos n} {x : ℕ} :
    x ∈ legalMoves p ↔ x ∈ p.pool ∧ IsPrimitive n (insert x p.claimed) := by
…
```
Mentions: Erdos872.GamePos, Erdos872.legalMoves, Erdos872.IsPrimitive
def Erdos872.applyMove Apply a move by claiming x and removing it from the unclaimed pool line 84 source
Source documentation
Apply a move by claiming x and removing it from the unclaimed pool.
This function is intentionally total: if x is not legal, it still returns the formal position obtained by inserting and erasing x. The minimax recursion below only calls it for x ∈ legalMoves p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos872.GamePos
Proof uses: Erdos872.GamePos.mk, Insert.insert, Finset, Erdos872.GamePos.claimed, Finset.erase, Erdos872.GamePos.pool
2 instances, coercions and auxiliary constants left out.
```
def applyMove {n : ℕ} (p : GamePos n) (x : ℕ) : GamePos n where
…
```
Mentions: Erdos872.GamePos
def Erdos872.startPos The empty starting position on $\{2, \dots, n\}$ line 89 source
Source documentation
The empty starting position on $\{2, \dots, n\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos872.GamePos
Proof uses: Erdos872.GamePos.mk, EmptyCollection.emptyCollection, Finset, Finset.Icc, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def startPos (n : ℕ) : GamePos n where
…
```
Mentions: Erdos872.GamePos
def Erdos872.gameValueAux Auxiliary finite minimax recursion with an explicit fuel bound line 99 source
Source documentation
Auxiliary finite minimax recursion with an explicit fuel bound.
At a Prolonger turn (turn = true) the recursion takes the maximum over legal moves; at a Shortener turn (turn = false) it takes the minimum. If there are no legal moves, or the fuel is exhausted, it returns the current final size p.claimed.card. Starting with fuel p.pool.card is sufficient because every played move erases the chosen pool element.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Erdos872.GamePos
2 instances, coercions and auxiliary constants left out.
```
def gameValueAux {n : ℕ} : ℕ → Bool → GamePos n → ℕ
  | 0, _turn, p => p.claimed.card
  | fuel + 1, turn, p =>
      let moves := legalMoves p
…
```
Mentions: Erdos872.GamePos, Erdos872.legalMoves
lemma Erdos872.gameValueAux_le Each move claims exactly one pool element, so the minimax value never exceeds the number of already claimed elements plus the number of still unclaimed elements line 114 source
Source documentation
Each move claims exactly one pool element, so the minimax value never exceeds the number of already claimed elements plus the number of still unclaimed elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Erdos872.GamePos, LE.le, Erdos872.gameValueAux, HAdd.hAdd, Finset.card, Erdos872.GamePos.claimed, Erdos872.GamePos.pool
Proof uses: Nat.recAux, id, OfNat.ofNat, Nat.le_add_right, Membership.mem, Finset, Erdos872.legalMoves, Bool.not, Erdos872.applyMove, And.left, Erdos872.IsPrimitive, Insert.insert, Iff.mp, And, Erdos872.mem_legalMoves, Finset.card_insert_le, Eq, Finset.erase, HSub.hSub, Finset.card_erase_of_mem and 28 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma gameValueAux_le {n : ℕ} (fuel : ℕ) (turn : Bool) (p : GamePos n) :
    gameValueAux fuel turn p ≤ p.claimed.card + p.pool.card := by
…
```
Mentions: Erdos872.GamePos, Erdos872.gameValueAux
def Erdos872.gameLength The minimax value of the primitive-set saturation game from p, with Prolonger to move line 148 source
Source documentation
The minimax value of the primitive-set saturation game from p, with Prolonger to move.
This is a genuine game-value definition rather than an uninterpreted placeholder. It unfolds the finite game tree up to p.pool.card moves; at each node Prolonger maximizes and Shortener minimizes the eventual terminal cardinality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos872.GamePos
Proof uses: Erdos872.gameValueAux, Finset.card, Erdos872.GamePos.pool, Bool.true
```
def gameLength {n : ℕ} : GamePos n → ℕ := fun p =>
…
```
Mentions: Erdos872.GamePos
def Erdos872.L The Erdős primitive-set game length on $\{2, \dots, n\}$ line 152 source
Source documentation
The Erdős primitive-set game length on $\{2, \dots, n\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Erdos872.gameLength, Erdos872.startPos
```
def L (n : ℕ) : ℕ := gameLength (startPos n)
…
```
Mentions: Erdos872.gameLength, Erdos872.startPos
theorem Erdos872.erdos_872.parts.i Erdős Problem 872, part (i) (weak form): there exists a constant $\epsilon > 0$ such that the game length is at least $\epsilon \cdot n$ for all sufficiently large $n$ sorry line 161 source
Source documentation
Erdős Problem 872, part (i) (weak form): there exists a constant $\epsilon > 0$ such that the game length is at least $\epsilon \cdot n$ for all sufficiently large $n$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, GE.ge, Erdos872.L, HMul.hMul, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_872.parts.i : answer(sorry) ↔
    ∃ ε > (0 : ℝ), ∀ᶠ n in atTop, (L n : ℝ) ≥ ε * n := by
…
```
Mentions: Erdos872.L
theorem Erdos872.erdos_872.parts.ii Erdős Problem 872, part (ii) (strong form): for every $\epsilon > 0$, the game length is at least $(1-\epsilon) \cdot n / 2$ for all sufficiently large $n$ sorry line 174 source
Source documentation
Erdős Problem 872, part (ii) (strong form): for every $\epsilon > 0$, the game length is at least $(1-\epsilon) \cdot n / 2$ for all sufficiently large $n$.
Status note: the forum thread (April-May 2026) records Shortener strategies giving $L(n) \leq (23/48 + o(1)) \cdot n$ (described in the thread as accepted as correct, with a Lean formalization in progress) and a claimed $L(n) \leq 0.19 \cdot n$, either of which would answer this question negatively under the Prolonger-first convention. Neither is published, so the statement is recorded here as the original Erdős question.

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, GE.ge, Erdos872.L, HDiv.hDiv, HMul.hMul, HSub.hSub, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_872.parts.ii : answer(sorry) ↔
    ∀ ε > (0 : ℝ), ∀ᶠ n in atTop, (L n : ℝ) ≥ (1 - ε) * n / 2 := by
…
```
Mentions: Erdos872.L
theorem Erdos872.erdos_872.trivial_upper_bound A trivial upper bound: a play can claim at most the $n - 1$ elements of $\{2, \dots, n\}$, so $L(n) \leq n - 1$ line 181 source
Source documentation
A trivial upper bound: a play can claim at most the $n - 1$ elements of $\{2, \dots, n\}$, so $L(n) \leq n - 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Erdos872.L, HSub.hSub
Proof uses: Trans.trans, Eq, HAdd.hAdd, Finset.card, Erdos872.GamePos.claimed, Erdos872.startPos, Erdos872.GamePos.pool, Erdos872.gameValueAux_le, Bool.true, Eq.mpr, id, congrFun', congrArg, Nat.card_Icc, Decidable.byContradiction, Not
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) :
    L n ≤ n - 1 := by
…
```
Mentions: Erdos872.L
theorem Erdos872.erdos_872.variants.prime_question Forum-related variant: how small can a maximal primitive subset of $\{2, \dots, n\}$ be? sorry line 195 source
Source documentation
Forum-related variant: how small can a maximal primitive subset of $\{2, \dots, n\}$ be? The set of primes in $\{2, \dots, n\}$ is a maximal primitive subset of size $\pi(n)$, and the forum thread asks whether this is the smallest possible for all $n \geq 2$. Equivalently: must every completed play of the saturation game, by both players and regardless of strategy, claim at least $\pi(n)$ elements? (Terminal positions of the game are exactly the maximal primitive subsets.)

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Finset, Maximal, Erdos872.IsPrimitive, LE.le, Finset.card, Finset.filter, Nat.Prime, Finset.Icc
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_872.variants.prime_question : answer(sorry) ↔
    ∀ n ≥ 2, ∀ A : Finset ℕ, Maximal (IsPrimitive n) A →
      ((Finset.Icc 2 n).filter Nat.Prime).card ≤ A.card := by
…
```
Mentions: Erdos872.IsPrimitive