Formal target: Corpus.WikipediaKomlosConjecture.komlos_conjecture

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

Exact formal statement

Exists.{1} fun K =>
  And (LT.lt.{0} 0 K)
    (∀ (n m : Nat) (v : Fin n → Fin m → Real),
      (∀ (i : Fin n), LE.le.{0} (Finset.sum.{0, 0} Finset.univ.{0} fun j => HPow.hPow.{0, 0, 0} (v i j) 2) 1) →
        Exists.{1} fun ε =>
          And (∀ (i : Fin n), Or (Eq.{1} (ε i) 1) (Eq.{1} (ε i) (-1)))
            (∀ (j : Fin m),
              LE.le.{0} (abs.{0} (Finset.sum.{0, 0} Finset.univ.{0} fun i => HMul.hMul.{0, 0, 0} (ε i) (v i j))) K))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record