Skip to content

Erdős problem 463

Start work

Is there a function ff with f(n)→∞f(n)\to\infty as n→∞n\to\infty such that, for all large nn, there is a composite number mm such that n+f(n)<m<n+p(m) n + f(n) < m < n + p(m) Here p(m)p(m) is the least prime factor of mm.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

463.lean

Retained formal statement1 of 1

Is there a function ff with f(n)→∞f(n)\to\infty as n→∞n\to\infty such that, for all large nn, there is a composite number mm such that n+f(n)<m<n+p(m) n + f(n) < m < n + p(m) Here p(m)p(m) is the least prime factor of mm.

FormalConjectures/ErdosProblems/463.leanErdos463.erdos_4634 linesExact file
True ↔  ∃ f,    ∃ (_ : Filter.Tendsto f Filter.atTop Filter.atTop),      ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, m.Composite ∧ n + f n < m ∧ m < n + m.minFac
OpenStatement only, no proof