Erdős problem 971
Let p(a, d) be the least prime congruent to a (mod d). Does there exist a constant c > 0 such that for all large d, p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/971.leanTrue ↔ ∃ c > 0, ∃ C > 0, ∀ᶠ (d : ℕ) in Filter.atTop, C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(Erdos971.leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.cardOpenStatement only, no proof