Beck–Fiala theorem and conjecture

formal-conjectures · wikipedia · ams-5

Discrepancy of bounded-degree set systems. Given sets $S_1, \dots, S_m \subseteq [n]$
such that every element of $[n]$ belongs to at most $t$ of the sets (the system has
*degree* at most $t$), one seeks a colouring $\chi \colon [n] \to \{-1, +1\}$ making
every set as balanced as possible, i.e. minimizing the *discrepancy*
$\max_i \left|\sum_{j \in S_i} \chi(j)\right|$.

The Beck–Fiala theorem (1981) states that every set system of degree at most $t \ge 1$
has discrepancy at most $2t - 1$. The Beck–Fiala conjecture asserts that the truth is
much stronger: the discrepancy of a degree-$t$ system is $O(\sqrt{t})$, with a constant
independent of $n$, $m$ and $t$.

Despite considerable attention the bound $2t - 1$ has been improved only slightly:
Bukh (2016) proved a bound of the form $2t - \log^* t$ (where $\log^*$ is the iterated
logarithm), and Banaszczyk's vector balancing theorem yields $O(\sqrt{t \log n})$.
The Komlós conjecture (see KomlosConjecture.lean) would imply the Beck–Fiala
conjecture, since scaling the incidence vectors of a degree-$t$ system by $1/\sqrt{t}$
produces vectors of Euclidean norm at most $1$.

**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$.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://en.wikipedia.org/wiki/Beck%E2%80%93Fiala_theorem
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1016/0166-218X
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1017/S0963548315000140
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1002/
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/BeckFialaConjecture.lean
Local target: Corpus.WikipediaBeckFialaConjecture.beck_fiala_conjecture
Source SHA-256: 89e5f42ab16943ec9ce3dbe008390b0d008739706f60b688bfb3250cb8d8cdd2
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record