All open problems
Source labels openChecked July 26, 2026

WikipediaCombinatorics

Komlós conjecture

The Komlós conjecture*

Mathematical statement

The Komlós conjecture*

There exists a universal constant K>0K > 0 such that for all n,mNn, m \in \mathbb{N} and all vectors v1,,vnRmv_1, \dots, v_n \in \mathbb{R}^m with vi21\|v_i\|_2 \le 1 (encoded here as jvij21\sum_j v_{ij}^2 \le 1), there exist signs εi{1,+1}\varepsilon_i \in \{-1, +1\} such that iεiviK\left\|\sum_i \varepsilon_i v_i\right\|_\infty \le K, i.e. iεivijK\left|\sum_i \varepsilon_i v_{ij}\right| \le K for every coordinate jj.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

komlos_conjecture

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem komlos_conjecture :     K : , 0 < K   (n m : ) (v : Fin n  Fin m  ),      ( i, ∑ j, (v i j) ^ 2  1)        ε : Fin n  , ( i, ε i = 1  ε i = -1)          j, |∑ i, ε i * v i j|  K := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References