Erdős problem 971 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

971.lean

Retained formal statement1 of 3

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?

FormalConjectures/ErdosProblems/971.leanErdos971.erdos_9717 linesExact file

1True ↔2  ∃ c > 0,3    ∃ C > 0,4      ∀ᶠ (d : ℕ) in Filter.atTop,5        C * ↑d.totient ≤6          ↑{a ∈ Finset.Iio d |7                a.Coprime d ∧ ↑(Erdos971.leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card

OpenStatement only, no proof

Sources

Search problems.science