Erdős problem 695

Let $q_1 < q_2 < \cdots$ be a sequence of primes such that $q_{i + 1} \equiv 1 \pmod{q_i}$ . Is it true that $\lim_{k \to \infty} q_k^{1/k} = \infty?$

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

695.lean

Retained formal statement2 of 2

Is there a sequence of primes $q_1 < q_2 < \cdots$ such that $q_{i + 1} \equiv 1 \pmod{q_i}$ and $q(k) \leq \exp(k (\log k)^{1 + o(1)})?$

FormalConjectures/ErdosProblems/695.leanErdos695.erdos_695.variants.upperBound6 linesExact file

1sorry ↔2  ∃ q,3    StrictMono q ∧4      (∀ (i : ℕ), Nat.Prime (q i)) ∧5        (∀ (i : ℕ), q (i + 1) % q i = 1) ∧6          ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (k : ℕ), ↑(q k) ≤ Real.exp ((↑k + 1) * Real.log (↑k + 1) ^ (1 + o k))

OpenStatement only, no proof