Erdős Problem 681

Reference: erdosproblems.com/681

def Erdos681.IsLPF (p m : ℕ) : Prop

IsLPF p m says that p is the least prime factor of m.

Equations

• Erdos681.IsLPF p m = (Nat.Prime p ∧ p ∣ m ∧ ∀ (q : ℕ), Nat.Prime q ∧ q ∣ m → p ≤ q)

theorem Erdos681.erdos_681 : sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k > 0, (n + k).Composite ∧ ∀ (p : ℕ), IsLPF p (n + k) → p > k ^ 2

Erdős problem 681. Is it true that for all large $n$ there exists $k$ such that $n + k$ is composite and $p(n+k) > k^2$, where $p(m)$ is the least prime factor of $m$ ?