linnik_constant_exact
Disprovednumber-theory
Linnik's theorem: The smallest prime in arithmetic progressions p ≡ a (mod q) satisfies p ≤ q^L. Best known: L ≤ 5 (Xylouris 2011). Conjectured L = 2.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem linnik_constant_exact :
∃ (L : ℝ),
L ≤ 2 ∧ 0 < L ∧
∀ q a : ℕ, 1 ≤ q → Nat.Coprime q a →
∃ p : ℕ, Nat.Prime p ∧ p % q = a ∧ (p : ℝ) ≤ (q : ℝ) ^ L := by
sorrySource