Erdős problem 695
Let be a sequence of primes such that . Is it true that
Sources
FormalConjectures/ErdosProblems/
695.lean
Retained formal statement
Is there a sequence of primes such that and
sorry ↔ ∃ q, StrictMono q ∧ (∀ (i : ℕ), Nat.Prime (q i)) ∧ (∀ (i : ℕ), q (i + 1) % q i = 1) ∧ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (k : ℕ), ↑(q k) ≤ Real.exp ((↑k + 1) * Real.log (↑k + 1) ^ (1 + o k))OpenStatement only, no proof