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 statement1 of 2

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?$

FormalConjectures/ErdosProblems/695.leanErdos695.erdos_6955 linesExact file

1sorry ↔2  ∀ {q : ℕ → ℕ},3    StrictMono q →4      (∀ (i : ℕ), Nat.Prime (q i)) →5        (∀ (i : ℕ), q (i + 1) % q i = 1) → Filter.Tendsto (fun k => ↑(q k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

OpenStatement only, no proof