skolem_conjecture
Proveddecidabilitygeometry
Skolem's conjecture (1937): If a linear recurrence sequence over ℤ has a zero, it is either eventually periodic with period k (so infinitely many zeros) or has finitely many zeros. The problem of deciding which case occurs is the Skolem problem. Decidability is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem skolem_conjecture (d : ℕ) (hd : 1 ≤ d)
(a c : Fin d → ℤ) (hc : ∀ i, Nat.Prime ((c i).natAbs))
(u : ℤ → ℤ)
(hrec : ∀ n : ℕ, u (n + d) = ∑ i, a i * u (n + i))
(hzero : ∃ n : ℕ, u n = 0) :
{n : ℕ | u n = 0}.Infinite ∨ {n : ℕ | u n = 0}.Finite := by
sorrySource