Erdős problem 985 · problems.science

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

Sources

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

2 retained statements2415f78e850a

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