Erdős problem 455

Let `q : ℕ → ℕ` be a strictly increasing sequence of primes such that `q (n + 2) - q (n + 1) ≥ q (n + 1) - q n`. Must `lim q n / (n ^ 2) = ∞`?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

455.lean

Retained formal statement1 of 2

Let q : ℕ → ℕ be a strictly increasing sequence of primes such that q (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Must lim q n / (n ^ 2) = ∞?

FormalConjectures/ErdosProblems/455.leanErdos455.erdos_4555 linesExact file

1True ↔2  ∀ (q : ℕ → ℕ),3    StrictMono q →4      (∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) →5        Filter.Tendsto (fun n => ↑(q n) / ↑n ^ 2) Filter.atTop Filter.atTop

OpenStatement only, no proof