Mathematical statement
The Komlós conjecture*
There exists a universal constant such that for all and all vectors with (encoded here as ), there exist signs such that , i.e. for every coordinate .
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
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
Pinned Formal Conjectures sourceformalizationWikipediabackgroundW. Banaszczyk, *Balancing vectors and Gaussian measures of n-dimensional convex bodies*,
Random Structures & Algorithms **12** (1998), 351–360backgroundJ. Spencer, *Six standard deviations suffice*,
Trans. Amer. Math. Soc. **289** (1985), 679–706background