Skip to content

Erdős problem 124

Start work

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 statement2 of 5

For any ε>0\varepsilon > 0, there exists an infinite sequence 2≤d0<d1<…2 \le d_0 < d_1 < \dots such that all sufficiently large integer can be written as ∑i∈Iai\sum_{i \in I} a_i where aia_i has only the digits 0,10, 1 when written in base did_i, but ∑i∈I1di−1≤ε\sum_{i \in I} \frac 1{d_i - 1} \le \varepsilon.

Proved by Melfi [Me04]

FormalConjectures/ErdosProblems/124.leanErdos124.erdos124.melfi_construction6 linesExact file
∀ {ε : ℝ},  0 < ε →    ∃ d,      StrictMono d ∧        ∑' (i : ℕ), (↑(d i) - 1)⁻¹ ≤ ε ∧          ∀ᶠ (n : ℕ) in Filter.atTop, ∃ I a, (∀ i ∈ I, a i ∈ Erdos124.sumsOfDistinctPowers (d i) 0) ∧ ∑ i ∈ I, a i = n
SolvedStatement only, no proof