Erdős problem 463
Is there a function with as such that, for all large , there is a composite number such that Here is the least prime factor of .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/463.leanTrue ↔ ∃ f, ∃ (_ : Filter.Tendsto f Filter.atTop Filter.atTop), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, m.Composite ∧ n + f n < m ∧ m < n + m.minFacOpenStatement only, no proof