Erdős Problem 385

Reference: erdosproblems.com/385

noncomputable def Erdos385.F (n : ℕ) : ℕ

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$.

Equations

• Erdos385.F n = sSup {x : ℕ | ∃ m < n, ∃ (_ : m.Composite), m + m.minFac = x}

theorem Erdos385.trivial_ub (n : ℕ) : ↑(F n) ≤ ↑n + √↑n

Note that trivially $F(n) \leq n + \sqrt{n}$.

theorem Erdos385.erdos_385.parts.i : sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, n < F n

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$. Is it true that $F(n)>n$ for all sufficiently large $n$?

theorem Erdos385.erdos_385.parts.ii : sorry ↔ Filter.Tendsto (fun (n : ℕ) => F n - n) Filter.atTop Filter.atTop

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$. Does $F(n) - n \to \infty$ as $n\to\infty$?

theorem Erdos385.erdos_385.variants.lb : sorry ↔ ∃ (e : ℕ → ℝ) (_ : e =o[Filter.atTop] 1), ∀ (n : ℕ), ↑n + (1 - e n) * √↑n ≤ ↑(F n)

A question of Erdős, Eggleton, and Selfridge, who write that in fact it is possible that this quantity is always at least $n+(1-o(1))\sqrt{n}$