Primitive roots of the form k² + 1

Every prime $p$ has a primitive root $0 < g < p$ of the form $k^2 + 1$, where $k$ is an integer.

Zhi-Wei Sun has offered a prize of RMB 2,000 for the first proof.

References:

• OEIS A239957
• Z.-W. Sun, "New observations on primitive roots modulo primes," arXiv:1405.0290 [math.NT], 2014.

theorem OEIS.A239957.conjecture (p : ℕ) (hp : Nat.Prime p) : ∃ (k : ℤ), k ^ 2 + 1 < ↑p ∧ orderOf (↑k ^ 2 + 1) = p - 1

Zhi-Wei Sun's Conjecture (A239957): Every prime $p$ has a primitive root $0 < g < p$ of the form $k^2 + 1$, where $k$ is an integer.