formal-conjectures · wikipedia · ams-5
The Komlós conjecture in discrepancy theory: there is a universal constant $K$ such
that for all $n, m$ and all vectors $v\_1, \dots, v\_n \in \mathbb{R}^m$ with
$\|v\_i\|\_2 \le 1$, there exist signs $\varepsilon\_i \in \{-1, +1\}$ such that
$$\left\|\sum\_{i=1}^n \varepsilon\_i v\_i\right\|\_\infty \le K.$$
The best known bound is due to Banaszczyk, who proved that one can always achieve
$O(\sqrt{\log n})$. The Beck–Fiala theorem on the discrepancy of sparse set systems
is a special case (up to scaling), and the conjecture would imply the Beck–Fiala
conjecture that set systems of degree $t$ have discrepancy $O(\sqrt{t})$.
**The Komlós conjecture**
There exists a universal constant $K > 0$ such that for all $n, m \in \mathbb{N}$ and
all vectors $v\_1, \dots, v\_n \in \mathbb{R}^m$ with $\|v\_i\|\_2 \le 1$ (encoded here as
$\sum\_j v\_{ij}^2 \le 1$), there exist signs $\varepsilon\_i \in \{-1, +1\}$ such that
$\left\|\sum\_i \varepsilon\_i v\_i\right\|\_\infty \le K$, i.e.
$\left|\sum\_i \varepsilon\_i v\_{ij}\right| \le K$ for every coordinate $j$.
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/Discrepancy_theory#Major_open_problems
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1002/
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1090/S0002-9947-1985-0784009-0
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/KomlosConjecture.lean
Local target: Corpus.WikipediaKomlosConjecture.komlos_conjecture
Source SHA-256: a922a2da903c76a2f3278c620f21e1a9c647a622bbae259692e2700b201afea6
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.
**The Komlós conjecture** There exists a universal constant $K > 0$ such that for all $n, m \in \mathbb{N}$ and all vectors $v\_1, \dots, v\_n \in \mathbb{R}^m$ with $\|v\_i\|\_2 \le 1$ (encoded here as $\sum\_j v\_{ij}^2 \le 1$), there exist signs $\varepsilon\_i \in \{-1, +1\}$
No public records on this page.
No public records on this page.