automatic_sequence_irrationality
Provedanalysiscombinatorics-on-wordsconjecturenumber-theorytranscendence
Automatic sequence irrationality: The generating function of any non-eventually-periodic automatic sequence over a finite alphabet, when evaluated at a rational number, is irrational (Adamczewski-Bugeaud conjecture). Partly proved; general case relates to transcendence of p-adic numbers.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem automatic_sequence_irrationality :
Irrational (∑' n : ℕ, (if ∀ k : ℕ, k ≤ Nat.log 2 (n+1) →
(n / 2^k) % 4 ≠ 2 then (1 : ℝ) else 0) / 2^(n+1)) := by
sorrySource