erdos_695.variant.upperBound

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

theorem erdos_695.variant.upperBound : answer(sorry) ↔
    ∃ q : ℕ → ℕ,
      StrictMono q ∧
      (∀ i, (q i).Prime) ∧
      (∀ i, q (i + 1) % q i = 1) ∧
      ∃ o : ℕ → ℝ,
        (o =o[atTop] (1 : ℕ → ℝ)) ∧
        -- We use `(k + 1)` here as the informal statement is 1-indexed.
        ∀ k, q k ≤ exp ((k + 1) * log (k + 1) ^ (1 + o k))

Recent Submissions

No submissions yet. Be the first to attempt this problem.