Papers With

← All papers
First page of An elementary proof of the Komlós conjecture

An elementary proof of the Komlós conjecture

Sankeerth Rao Karingula, Shachar Lovett

math.CO Sep 17, 2026 · v2 cs.CC
formalization combinatorics probability
Read PDF arXiv abstract
TL;DR
A third party (Dahia) formalized the paper's proof of the Komlós conjecture with constant 36 in Lean 4, with a public GitHub repository.
Abstract
We give an elementary proof of the Komlós conjecture by simplifying the recent proof of Guo, Fang, and Lu. We show that any vectors $v_1,\ldots,v_n\in\mathbb{R}^d$ with $\|v_i\|_2\le1$ admit signs $\varepsilon_i\in\{-1,1\}$ such that $\|\sum_{i=1}^n\varepsilon_i v_i\|_\infty\le36$. The proof uses only elementary combinatorial and probabilistic arguments and basic calculus.
Problem

The Komlós conjecture asks for a universal constant C such that any unit-norm vectors in R^d admit signs whose signed sum has max-norm at most C. A recent proof by Guo, Fang, and Lu settled it, and the authors seek a simpler argument.

Approach

The bound is reduced to finding a finitely supported distribution in a cube that is nearly invariant under shifts by multiples of each vector. Induction on the number of vectors uses a splitting operator that adds a binary coordinate, followed by a pullback to signed sums. The near-invariant distribution comes from a product density (a squared tent function) whose square root has small directional derivatives, rounded to a grid.

Results

Any vectors with Euclidean norm at most 1 admit signs with the max-norm of the signed sum at most 36, using only elementary combinatorics, probability, and calculus. The proof was formalized in Lean 4 by Dahia.