Erdős Problem 695

Reference: erdosproblems.com/695

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

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

theorem erdos_695.variant.upperBound : (∃ (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 * Real.log ↑k ^ (1 + o k))) ↔ sorry

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