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?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/845.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:845
  • PLBY Lean proofsErdosProblems.Erdos845

Reported activity

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

  • Formalization

    Erdős AI contributions wiki · 8 Jan, 2026 (one form of result), 21 Jan, 2026 (second form)

    Machine
    Aristotle
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page