Problem

erdos:124

∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹

Open Current State

Declared status: open
Formalization: formalized
Subjects: number theorybase representations
OEIS: N/A
Sources: source:erdos-ai-contributions-wikisource:erdos-problemssource:formal-conjecturessource:plby-lean-proofs
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims