The Beck--Fiala theorem: discrepancy at most $2t-1$

Proved

Komlos.beck_fiala

by Shuze Chen · Sep 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

beck-fialadiscrepancyset-systems

(Beck--Fiala 1981.) Let $A$ be an $m \times n$ matrix with entries in $\{0, 1\}$ — the incidence matrix of $m$ sets over $n$ elements — in which every column has at most $t \ge 1$ ones: every element belongs to at most $t$ sets. Then there are signs $\varepsilon_j \in \{\pm 1\}$ with

\Big|\sum_{j=1}^{n} A_{ij}\,\varepsilon_j\Big| \le 2t - 1 \qquad \text{for every set } i.

The bound depends only on the degree $t$ , not on $m$ or $n$ . The hypothesis $t \ge 1$ is necessary for the formal statement (a degree- $0$ system has discrepancy $0$ , but $2t-1$ would be $-1$ ).

Preamble

import Mathlib
import Definitions.Def_Komlos_model

Formal statement

namespace Komlos

theorem beck_fiala (t n m : ℕ) (ht : 1 ≤ t) (A : Fin m → Fin n → ℝ)
    (h01 : ∀ i j, A i j = 0 ∨ A i j = 1)
    (hdeg : ∀ j, ({i | A i j = 1} : Finset (Fin m)).card ≤ t) :
    ∃ ε : Fin n → ℝ, IsSignVector ε ∧
      ∀ i, |∑ j, A i j * ε j| ≤ 2 * (t : ℝ) - 1 := by sorry

end Komlos

Source

Beck--Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981) 1-8, Theorem: disc at most 2t-1 for degree-t set systems, https://doi.org/10.1016/0166-218X(81)90022-6

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back of Komlos.beck_fiala.

The statement quantifies over three natural numbers $t, n, m$ (any of which may be $0$ , except that $t$ is constrained by a hypothesis below), a hypothesis $1 \le t$ , and a real matrix $A$ with $m$ rows and $n$ columns, i.e. a function assigning a real number $A_{i,j}$ to each row index $i \in \{0, \dots, m-1\}$ and column index $j \in \{0, \dots, n-1\}$ . It assumes:

(0/1 entries) for every row $i$ and column $j$ , either $A_{i,j} = 0$ or $A_{i,j} = 1$ ;
(column degree bound) for every column $j$ , the number of row indices $i$ with $A_{i,j} = 1$ is at most $t$ .

Under these hypotheses it asserts the existence of a vector $\varepsilon = (\varepsilon_0, \dots, \varepsilon_{n-1})$ of real numbers which is a sign vector — here this is the unfolded content of the custom predicate IsSignVector, meaning that for every index $j$ , either $\varepsilon_j = 1$ or $\varepsilon_j = -1$ — such that for every row $i$ ,

\left| \sum_{j=0}^{n-1} A_{i,j}\, \varepsilon_j \right| \;\le\; 2t - 1,

where the bound is the non-strict inequality $\le$ , the sum ranges over all $n$ columns, and $2t - 1$ is computed in the real numbers after coercing the natural number $t$ (so no truncated natural-number subtraction occurs; since $1 \le t$ , the bound is at least $1$ ).

Degenerate cases silently included by the quantifiers: if $m = 0$ there are no rows, so the final condition on rows holds vacuously (any sign vector works); if $n = 0$ the sign vector is the empty vector, every sum is the empty sum $0$ , and the bound $0 \le 2t - 1$ holds since $t \ge 1$ . Nothing in the statement requires the rows (viewed as sets of columns) to be distinct or nonempty, and the hypothesis $1 \le t$ excludes only the case $t = 0$ . The declaration is stated with its proof omitted (sorry), so the file records the claim, not a completed proof.

Human review

Endorsed by Community (Bot) · Sep 3, 2026
Endorsed by Shuze Chen · Sep 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Beck--Fiala theorem: discrepancy at most 2t−12t-12t−1

The Beck--Fiala theorem: discrepancy at most $2t-1$