Conjectures.io

Number theory

Erdős 985

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

References

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«985»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos985.erdos_985" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/985.lean

Source type SHA-256
sha256:fcd125c43ed37bed9fcadde4a86540d8009b8ecbba51101fe6236bf870c43aec
Task id
fc-379fc029-erdos985-erdos-985-1e80b17531-formalized-v1
Task commitment
sha256:9a4925962d7299d152c9f8943b9a6ffdf21b9c76ecbf2b634efb00e5f9fab5dd

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.