All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 872: Prime Question

Forum-related variant: how small can a maximal primitive subset of {2,,n}\{2, \dots, n\} be? The set of primes in {2,,n}\{2, \dots, n\} is a maximal primitive subset of size π(n)\pi(n), and the forum thread asks whether this is the smallest possible for all $n \geq 2...

Mathematical statement

Forum-related variant: how small can a maximal primitive subset of {2,,n}\{2, \dots, n\} be? The set of primes in {2,,n}\{2, \dots, n\} is a maximal primitive subset of size π(n)\pi(n), and the forum thread asks whether this is the smallest possible for all n2n \geq 2. Equivalently: must every completed play of the saturation game, by both players and regardless of strategy, claim at least π(n)\pi(n) elements? (Terminal positions of the game are exactly the maximal primitive subsets.)

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_872.variants.prime_question

Canonical source
Complete statement target, proof intentionally absentLean 4
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  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References