Erdős Problem 872: Prime Question
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 $n \geq 2...
Mathematical 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.)
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
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