Erdős problem 124 · problems.science

Let $k \ne 0$ and $3\leq d_1 < d_2 < \cdots < d_r$ be integers of gcd equal to $1$ such that $\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 $\sum_i c_ia_i$ where $c_i \in \{0, 1\}$ and $a_i$ is divisible by $d_i ^ k$ and has only the digits $0, 1$ when written in base $d_i$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

124.lean

Retained formal statement1 of 5

Let $3\leq d_1 < d_2 < \cdots < d_r$ be integers such that all sufficiently large integers can be written as a sum of the shape $\sum_i c_ia_i$ where $c_i \in \{0, 1\}$ and $a_i$ has only the digits $0, 1$ when written in base $d_i$ . Then $\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.$

Reported by Burr, Erdős, Graham, and Li [BEGL96] as an observation of Pomerance

FormalConjectures/ErdosProblems/124.leanErdos124.erdos124.converse3 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science