Skip to content

Erdős problem 385

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

385.lean

Retained formal statement1 of 4

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

FormalConjectures/ErdosProblems/385.leanErdos385.erdos_385.parts.i1 lineExact file
sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, n < Erdos385.F n
OpenStatement only, no proof