All open problems
Source labels openChecked July 26, 2026

WikipediaNumber theory

Artin's conjecture on primitive roots: Part Ii Power Squarefree Part Not Modeq One

Artin's Conjecture on Primitive Roots*, second half, power version If a=bma = b^m is a perfect odd power of a number bb whose squarefree part b0≢1(mod4)b_0\not\equiv 1 \pmod{4}, then the density of the set S(a)S(a) of primes pp such that aa is a primitive root mod...

Mathematical statement

Artin's Conjecture on Primitive Roots*, second half, power version If a=bma = b^m is a perfect odd power of a number bb whose squarefree part b0≢1(mod4)b_0\not\equiv 1 \pmod{4}, then the density of the set S(a)S(a) of primes pp such that aa is a primitive root modulo pp is given by Cpmp(p2)p2p1C\prod_{p \mid m} \frac{p(p - 2)}{p^2 - p - 1}, where CC is Artin's constant.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem artin_primitive_roots.variants.part_ii_power_squarefreePart_not_modeq_one    (a m b : ) (ha : a = b ^ m) (hb :  u v, 1 < u  b  v^u) (hm₁ : 1 < m)    (hm₂ : Odd m) (hb' : ¬ b.squarefreePart1 [MOD 4]) :    (S a).HasDensity (ArtinConstant * powCorrectionFactor m) {p | p.Prime} := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References