Černý Conjecture

Theorem · shitov_upper_bound

**Shitov's bound (2019)**: Every synchronizing DFA with $n$ states admits a synchronizing word of length at most $\left(\frac{7}{48} + \frac{2 \cdot 15625}{1597536}\right) n^3 + o(n^3)$ , where the $o(n^3)$ term is uniform over all alphabets. This is the best known upper bound towards the Černý conjecture.

Formal statement · Lean 4.lean

theorem shitov_upper_bound :
    ∃ f : ℝ → ℝ, f =o[atTop] (fun n : ℝ => n ^ 3) ∧
    ∀ {α : Type*} {σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing) ,
    ∃ w : List α, M.IsSynchronizingWord w ∧
    (w.length : ℝ) ≤ (7 / 48 + 2 * 15625 / 1597536) * (Fintype.card σ : ℝ) ^ 3
      + f (Fintype.card σ : ℝ) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗