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

Open selected source

FormalConjectures/ErdosProblems/

985.lean

Retained formal statement1 of 2

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

FormalConjectures/ErdosProblems/985.leanErdos985.erdos_9851 lineExact file

1sorry ↔ ∀ (p : ℕ), Nat.Prime p → p ≠ 2 → ∃ q, Nat.Prime q ∧ q < p ∧ orderOf ↑q = p - 1

OpenStatement only, no proof