Number theory

Erdős problem 695 - upper Bound

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

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«695»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos695.erdos_695.variants.upperBound" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∃ 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))

Original conjecture source: FormalConjectures/ErdosProblems/695.lean

Source type SHA-256: sha256:5d3b0dcca310b5be635b9260e38a0b7930d25a971b364e4543feb1a67468077a
Task id: fc-v2-variants-upperbound-b30ca9203ee773770868a876-formalized
Task commitment: sha256:f84f20de14d5dd959ca91075104b4b27dbfda9e53a92bc9128745cae7109e12d

References

erdosproblems.com/695

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

True ↔ ∃ 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))