Formal target: Corpus.OEIS239957.conjecture

**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.

Exact formal statement

∀ (p : Nat), Nat.Prime p → Corpus.OEIS239957.A p

This target is a formal statement, not a proof of the problem.

Environment availability: available.