Beck–Fiala theorem and conjecture

Conjecture · beck_fiala_conjecture

**The Beck–Fiala conjecture**

There exists a universal constant $C > 0$ such that every set system $S_1, \dots, S_m \subseteq [n]$ of degree at most $t$ admits a colouring $\chi \colon [n] \to \{-1, +1\}$ with $\left|\sum_{j \in S_i} \chi(j)\right| \le C \sqrt{t}$ for every $i$ .

Formal statement · Lean 4.lean

theorem beck_fiala_conjecture :
    ∃ C : ℝ, 0 < C ∧ ∀ (n m t : ℕ) (S : Fin m → Finset (Fin n)),
      (∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) →
      ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
        ∀ i, |∑ j ∈ S i, χ j| ≤ C * Real.sqrt t := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗