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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

971.lean

Retained formal statement2 of 3

Erdős [Er49c] proved that the statement in erdos_971 holds for infinitely many values of d.

[Er49c] Erdős, P., _On some applications of Brun's method_. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

FormalConjectures/ErdosProblems/971.leanErdos971.erdos_971.variants.infinite_sequence6 linesExact file

1∃ c > 0,2  ∃ C > 0,3    {d |4        C * ↑d.totient ≤5          ↑{a ∈ Finset.Iio d |6                a.Coprime d ∧ ↑(Erdos971.leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card}.Infinite

SolvedStatement only, no proof