Skip to content

Erdős problem 385

Start work

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 statement2 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. Does F(n)−n→∞F(n) - n \to \infty as n→∞n\to\infty?

FormalConjectures/ErdosProblems/385.leanErdos385.erdos_385.parts.ii1 lineExact file
sorry ↔ Filter.Tendsto (fun n => Erdos385.F n - n) Filter.atTop Filter.atTop
OpenStatement only, no proof