Erdős problem 985
Is it true that, for every prime , there is a prime which is a primitive root modulo ?
Sources
FormalConjectures/ErdosProblems/
985.lean
Retained formal statement
Heath-Brown proved that at least one of 2, 3, or 5 is a primitive root for infinitely many primes .
{p | Nat.Prime p ∧ (orderOf 2 = p - 1 ∨ orderOf 3 = p - 1 ∨ orderOf 5 = p - 1)}.InfiniteSolvedStatement only, no proof