Skip to content

Erdős problem 124

Let k≠0k \ne 0 and 3≤d1<d2<⋯<dr3\leq d_1 < d_2 < \cdots < d_r be integers of gcd equal to 11 such that ∑1≤i≤r1di−1≥1.\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1. Can all sufficiently large integers be written as a sum of the shape ∑iciai\sum_i c_ia_i where ci∈{0,1}c_i \in \{0, 1\} and aia_i is divisible by dikd_i ^ k and has only the digits 0,10, 1 when written in base did_i?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

124.lean

Retained formal statement3 of 5

Let k≠0k \ne 0 and 3≤d1<d2<⋯<dr3\leq d_1 < d_2 < \cdots < d_r be integers of gcd equal to 11 such that ∑1≤i≤r1di−1≥1.\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1. Can all sufficiently large integers be written as a sum of the shape ∑iciai\sum_i c_ia_i where ci∈{0,1}c_i \in \{0, 1\} and aia_i is divisible by dikd_i ^ k and has only the digits 0,10, 1 when written in base did_i?

Conjectured by Burr, Erdős, Graham, and Li [BEGL96]

FormalConjectures/ErdosProblems/124.leanErdos124.erdos124.ne_zero7 linesExact file
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 k
OpenStatement only, no proof