Erdős problem 290
Let . Must there exist some such that with and ? If so, how does this grow with ?
Sources
FormalConjectures/ErdosProblems/
290.lean
Retained formal statement
Let . Must there exist some such that with and ? If so, how does this grow with ?
This was resolved in the affirmative by van Doorn [vD24], who proved always exists, and in fact . Indeed, if then one can take . van Doorn also proves that , and considers various generalisations of the original problem.
True ↔ ∀ (a : ℕ), 1 ≤ a → ∃ b, a < b ∧ Erdos290.harmonicDen a (b + 1) < Erdos290.harmonicDen a b