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.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/650.lean∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊SolvedStatement only, no proof
Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:650 - PLBY Lean proofs
ErdosProblems.Erdos650
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine
AI alongside literature
- Machine
argument
- Machine
- Reported outcome