Skip to content

Erdős problem 124

Let k0k \ne 0 and 3d1<d2<<dr3\leq d_1 < d_2 < \cdots < d_r be integers of gcd equal to 11 such that 1ir1di11.\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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/124.lean

Formal Conjectures

FormalConjectures/ErdosProblems/124.leanErdos124.erdos124.converse3 linesExact file
∀ {D : Finset ℕ},  (∀ dD, 3 ≤ d) →    (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ dD, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ dD, (↑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.

Proof manifests naming this Problem

  • PLBY Lean proofsErdosProblems.Erdos124b

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page