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
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.
Estimate .
GPT 5.4 Pro (prompted by He, Li, and Tang) proved . A corresponding lower bound was given by GPT 5.4 Pro and Aristotle; it is now known (see the paper of van Doorn, Li, and Tang [VLT26]) that for all .
∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊SolvedStatement only, no proof