stark_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result stark_conjecture is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Stark's conjecture (1971): For Abelian extensions of number fields, the leading Taylor coefficient of Artin L-functions at s=0 is expressed via special algebraic units (Stark units). Proved for rank 1 (Stark 1977); higher rank open.

Why this node was retired

The posted statement is

import Mathlib

theorem stark_conjecture (n : ℕ) (hn : 1 ≤ n)
    (K : Type*) [Field K] [NumberField K]
    (zeta_K : ℂ → ℂ)
    (horder : ∃ (r : ℕ) (eps : ℝ) (A : ℝ),
      0 < r ∧ 0 < eps ∧ 0 < A ∧
      ∀ s : ℂ, 0 < s.re → s.re < eps →
        zeta_K s = s ^ r * A * (1 + s)) :
    ∃ (units : Fin n → ℝ) (regulator : ℝ),
      regulator = Matrix.det (Matrix.of (fun i j => Real.log (units i))) ∧
      ∀ s : ℂ, True := by
  sorry

The goal is ∃ (units : Fin n → ℝ) (regulator : ℝ), regulator = Matrix.det (…) ∧ ∀ s : ℂ, True. The second conjunct is True, and the first merely names the determinant of a matrix built from arbitrary reals — the units are not units of any ring. No Artin L-function and no leading coefficient at s = 0 appear.

What a faithful statement would require

The conclusion must relate the leading Taylor coefficient of the Artin L-function at s = 0 to a regulator formed from actual S-units, up to an algebraic factor.

No corrected replacement node exists yet.