Number theory

Erdős problem 124 - ne zero

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

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

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«124»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos124.erdos124.ne_zero" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/124.lean

Source type SHA-256: sha256:1423a393df40cb7f5f4543388eb5a5532c0236f65fee237917b0888180f041b1
Task id: fc-v2-erdos124-ne-zero-6bb73d7003d7de78284cb7b8-formalized
Task commitment: sha256:9f548a302ffa8c9c72aaf22ea661e19c59634e0d80d4443200bcd9607c52645a

References

erdosproblems.com/124

[BEGL96] Burr, S. A. and Erdős, P. and Graham, R. L. and Li, W. Wen-Ching, Complete sequences of sets of integer powers. Acta Arith. (1996), 133-138.

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord