Skip to content

Erdős problem 463

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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/463.lean

Formal Conjectures

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

Continue