erdős #1137
Let , where denotes the th prime. Is it true thatas ?
Worked, still open.
number theory · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 11 · open (literature)
theorem erdos_1137 :
answer(sorry) ↔
Tendsto (fun x ↦
(((range x).sup (fun n ↦ (primeGap n) * (primeGap (n - 1))) : ℕ) : ℝ) /
(((range x).sup primeGap : ℕ) : ℝ) ^ 2) atTop (𝓝 0)formal-conjectures/1137.lean ↗oeis
A005250 — Record gaps between primes.1,2,4,6,8,14,18,20,22,34,36,44,52,72,86,96,112,114,118,132,148,154,180,210,220,222,234,248,250,282,288,292,320,336,354,3A083550 — Product of 2 consecutive prime differences of two successive terms of A001223.2,4,8,8,8,8,8,24,12,12,24,8,8,24,36,12,12,24,8,12,24,24,48,32,8,8,8,8,56,56,24,12,20,20,12,36,24,24,36,12,20,20,8,8,24,1
status
open