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

FormalConjectures/ErdosProblems/

455.lean

Retained formal statement2 of 2

Let q : ℕ → ℕ be a strictly increasing sequence of primes such that q (n + 2) - q (n + 1) ≥ q (n + 1) - q n. Then liminf q n / (n ^ 2) > 0.352, and this is proved in [Ri76].

FormalConjectures/ErdosProblems/455.leanErdos455.erdos_455.variants.liminf4 linesExact file

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

SolvedStatement only, no proof