Skip to content

Erdős problem 845

Let C>0C > 0. Is it true that the set of integers of the form n=b1+⋯+btn = b_1 + \cdots + b_t, with b1<⋯<btb_1 < \cdots < b_t, where bi=2ki3lib_i = 2^{k_i}3^{l_i} for 1≤i≤t1 \leq i\leq t and bt≤Cb1b_t \leq Cb_1 has density 00?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

845.lean

Retained formal statement1 of 1

Let C>0C > 0. Is it true that the set of integers of the form n=b1+⋯+btn = b_1 + \cdots + b_t, with b1<⋯<btb_1 < \cdots < b_t, where bi=2ki3lib_i = 2^{k_i}3^{l_i} for 1≤i≤t1 \leq i\leq t and bt≤Cb1b_t \leq Cb_1 has density 00?

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

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/845.leanErdos845.erdos_8457 linesExact file
False ↔  ∀ (C : ℝ),    0 < C →      have f := fun x =>        match x with        | (k, l) => 2 ^ k * 3 ^ l;      {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.