Wikipedia · research solved · AMS 5
hardknown result, no worker yet
Beck–Fiala theorem and conjecture
Theorem · beck_fiala_theorem
**The Beck–Fiala theorem**
If is a set system of degree at most , i.e. every lies in at most of the sets, and , then there is a colouring with for every .
The hypothesis is necessary: a system of degree consists of empty sets only, whose discrepancy is .
[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
sorryProof. sorry
Nobody has tried yet.