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:

• erdosproblems.com/872
• erdosproblems.com/forum/thread/872

def Erdos872.IsPrimitive (n : ℕ) (A : Finset ℕ) : Prop

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.

Equations

• Erdos872.IsPrimitive n A = (A ⊆ Finset.Icc 2 n ∧ ∀ a ∈ A, ∀ b ∈ A, a ≠ b → ¬a ∣ b)

structure Erdos872.GamePos (n : ℕ) : Type

A game position consists of the already claimed set and the still unclaimed pool.

• claimed : Finset ℕ
• pool : Finset ℕ

def Erdos872.legalMoves {n : ℕ} (p : GamePos n) : Finset ℕ

The legal moves from a position: unclaimed elements whose insertion preserves primitiveness.

Equations

• Erdos872.legalMoves p = {x ∈ p.pool | Erdos872.IsPrimitive n (insert x p.claimed)}

theorem Erdos872.mem_legalMoves {n : ℕ} {p : GamePos n} {x : ℕ} : x ∈ legalMoves p ↔ x ∈ p.pool ∧ IsPrimitive n (insert x p.claimed)

Membership in legalMoves: a legal move is a pool element whose insertion preserves primitiveness.

def Erdos872.applyMove {n : ℕ} (p : GamePos n) (x : ℕ) : GamePos n

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.

Equations

• Erdos872.applyMove p x = { claimed := insert x p.claimed, pool := p.pool.erase x }

def Erdos872.startPos (n : ℕ) : GamePos n

The empty starting position on $\{2, \dots, n\}$.

Equations

• Erdos872.startPos n = { claimed := ∅, pool := Finset.Icc 2 n }

def Erdos872.gameValueAux {n : ℕ} : ℕ → Bool → GamePos n → ℕ

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.

Equations

• One or more equations did not get rendered due to their size.
• Erdos872.gameValueAux 0 x✝¹ x✝ = x✝.claimed.card

theorem Erdos872.gameValueAux_le {n : ℕ} (fuel : ℕ) (turn : Bool) (p : GamePos n) : gameValueAux fuel turn p ≤ p.claimed.card + p.pool.card

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.

def Erdos872.gameLength {n : ℕ} : GamePos n → ℕ

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.

Equations

• Erdos872.gameLength p = Erdos872.gameValueAux p.pool.card true p

def Erdos872.L (n : ℕ) : ℕ

The Erdős primitive-set game length on $\{2, \dots, n\}$.

Equations

• Erdos872.L n = Erdos872.gameLength (Erdos872.startPos n)

theorem Erdos872.erdos_872.parts.i : sorry ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(L n) ≥ ε * ↑n

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

theorem Erdos872.erdos_872.parts.ii : sorry ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(L n) ≥ (1 - ε) * ↑n / 2

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.

theorem Erdos872.erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) : L n ≤ n - 1

A trivial upper bound: a play can claim at most the $n - 1$ elements of $\{2, \dots, n\}$, so $L(n) \leq n - 1$.

theorem Erdos872.erdos_872.variants.prime_question : sorry ↔ ∀ n ≥ 2, ∀ (A : Finset ℕ), Maximal (IsPrimitive n) A → (Finset.filter Nat.Prime (Finset.Icc 2 n)).card ≤ A.card

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