Erdős problem 845 · problems.science

Let $C > 0$ . Is it true that the set of integers of the form $n = b_1 + \cdots + b_t$ , with $b_1 < \cdots < b_t$ , where $b_i = 2^{k_i}3^{l_i}$ for $1 \leq i\leq t$ and $b_t \leq Cb_1$ has density $0$ ?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

845.lean

Retained formal statement1 of 1

van Doorn and Everts [vDEv25] have disproved this with $C=6$ - in fact, they prove that all integers can be written as such a sum in which $b_t<6b_1$ .

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/845.leanErdos845.erdos_8457 linesExact file

1False ↔2  ∀ (C : ℝ),3    0 < C →4      have f := fun x =>5        match x with6        | (k, l) => 2 ^ k * 3 ^ l;7      {x | ∃ B, ∃ (h : B.Nonempty) (_ : ↑(B.sup f) ≤ C * ↑(B.inf' h f)), ∑ x ∈ B, f x = x}.HasDensity 0

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