Erdős problem 124
Let and be integers of gcd equal to such that Can all sufficiently large integers be written as a sum of the shape where and is divisible by and has only the digits when written in base ?
Sources
FormalConjectures/ErdosProblems/
124.lean
Retained formal statement
Let and be integers of gcd equal to such that Can all sufficiently large integers be written as a sum of the shape where and is divisible by and has only the digits when written in base ?
Conjectured by Burr, Erdős, Graham, and Li [BEGL96]
True ↔ ∀ (k : ℕ), k ≠ 0 → ∀ (D : Finset ℕ), (∀ d ∈ D, 3 ≤ d) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹ → D.gcd id = 1 → ∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d kOpenStatement only, no proof