Erdős problem 455 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

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

Sources

Search problems.science