Erdős problem 650
Let be such that if has then every interval in of length contains many distinct integers where each is divisible by some , where are distinct.
Sources
FormalConjectures/ErdosProblems/
650.lean
Retained formal statement
Erdős and Selfridge proved (see [Er78] and [Er86c]) that , which implies for all .
∀ (m : ℕ), Erdos650.f (m ^ 2) ≤ 2 * mSolvedStatement only, no proof