Erdős problem 872
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.
Sources
FormalConjectures/ErdosProblems/
872.lean
Retained formal statement
Forum-related variant: how small can a maximal primitive subset of be? The set of primes in is a maximal primitive subset of size , and the forum thread asks whether this is the smallest possible for all . Equivalently: must every completed play of the saturation game, by both players and regardless of strategy, claim at least elements? (Terminal positions of the game are exactly the maximal primitive subsets.)
True ↔ ∀ n ≥ 2, ∀ (A : Finset ℕ), Maximal (Erdos872.IsPrimitive n) A → (Finset.filter Nat.Prime (Finset.Icc 2 n)).card ≤ A.cardOpenStatement only, no proof