Skip to content

Erdős problem 680

Is it true that, for all sufficiently large nn, there exists some kk such that p(n+k)>k2+1, p(n+k)>k^2+1, where p(m)p(m) denotes the least prime factor of mm?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

680.lean

Retained formal statement2 of 2

Can one prove this is false if we replace k2+1k^2+1 by e(1+ϵ)k+Cϵe^{(1+\epsilon)\sqrt{k}}+C_\epsilon, for all ϵ>0\epsilon>0, where Cϵ>0C_\epsilon>0 is some constant?

FormalConjectures/ErdosProblems/680.leanErdos680.erdos_680.parts.ii1 lineExact file
True ↔ ∀ ε > 0, ∃ C > 0, ¬∀ᶠ (n : ℕ) in Filter.atTop, ∃ k, k ≠ 0 ∧ ↑(n + k).minFac > Real.exp ((1 + ε) * √↑k) + C
OpenStatement only, no proof