erdős #845
Let . Is it true that the set of integers of the formwhere for and has density ?
Worked, still open.
number theory · solved · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · solved (literature)
theorem erdos_845 :
answer(False) ↔
∀ᵉ (C : ℝ) (hC : 0 < C),
let f : ℕ × ℕ → ℕ := fun (k, l) ↦ 2 ^ k * 3 ^ l
{ ∑ x ∈ B, f x | (B : Finset (ℕ × ℕ)) (h : B.Nonempty)
(hB : B.sup f ≤ C * B.inf' h f) }.HasDensity 0formal-conjectures/845.lean ↗status
solved