Wikipedia · research solved · AMS 5

hardknown result, no worker yet

Beck–Fiala theorem and conjecture

Theorem · beck_fiala_theorem

**The Beck–Fiala theorem**

If S1,…,Sm⊆[n]S_1, \dots, S_m \subseteq [n] is a set system of degree at most tt, i.e. every j∈[n]j \in [n] lies in at most tt of the sets, and t≥1t \ge 1, then there is a colouring χ ⁣:[n]→{−1,+1}\chi \colon [n] \to \{-1, +1\} with ∣∑j∈Siχ(j)∣≤2t−1\left|\sum_{j \in S_i} \chi(j)\right| \le 2t - 1 for every ii.

The hypothesis t≥1t \ge 1 is necessary: a system of degree 00 consists of empty sets only, whose discrepancy is 0>2⋅0−10 > 2 \cdot 0 - 1.

[J. Beck and T. Fiala, *"Integer-making" theorems*, Discrete Applied Mathematics **3** (1981), 1–8.]

Formal statement · Lean 4.lean
theorem beck_fiala_theorem (n m t : ℕ) (ht : 1 ≤ t) (S : Fin m → Finset (Fin n))
    (hdeg : ∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) :
    ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
      ∀ i, |∑ j ∈ S i, χ j| ≤ 2 * (t : ℝ) - 1 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗