Erdős problem 680
Is it true that, for all sufficiently large , there exists some such that where denotes the least prime factor of ?
Sources
FormalConjectures/ErdosProblems/
680.lean
Retained formal statement
Is it true that, for all sufficiently large , there exists some such that where denotes the least prime factor of ?
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k, k ≠ 0 ∧ (n + k).minFac > k ^ 2 + 1OpenStatement only, no proof