Erdős problem 985

Is it true that, for every prime $p$ , there is a prime $q \leq p$ which is a primitive root modulo $p$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

985.lean

Retained formal statement2 of 2

Heath-Brown proved that at least one of 2, 3, or 5 is a primitive root for infinitely many primes $p$ .

FormalConjectures/ErdosProblems/985.leanErdos985.erdos_985.variants.two_three_five_primitive_root1 lineExact file

1{p | Nat.Prime p ∧ (orderOf 2 = p - 1 ∨ orderOf 3 = p - 1 ∨ orderOf 5 = p - 1)}.Infinite

SolvedStatement only, no proof