Erdős problem 681
Erdős problem 681. Is it true that for all large there exists such that is composite and , where is the least prime factor of ?
Sources
FormalConjectures/ErdosProblems/
681.lean
Retained formal statement
Erdős problem 681. Is it true that for all large there exists such that is composite and , where is the least prime factor of ?
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k > 0, (n + k).Composite ∧ ∀ (p : ℕ), Erdos681.IsLPF p (n + k) → p > k ^ 2OpenStatement only, no proof