Erdős Problem 985

Reference: erdosproblems.com/985

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

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

theorem Erdos985.erdos_985.variants.two_three_five_primitive_root : {p : ℕ | Nat.Prime p ∧ (orderOf 2 = p - 1 ∨ orderOf 3 = p - 1 ∨ orderOf 5 = p - 1)}.Infinite

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