The Euclidean Steinitz–Bergström bound

1 paperLean

Proves that any finite sequence in the Euclidean unit ball of ℝ^d admits signs keeping every partial sum within \(C\sqrt d\), independently of length. Consequently every zero-sum family can be reordered with the same bound on unsigned partial sums. A matching lower bound gives the optimal order \(S_2(d)=\Theta(\sqrt d)\).

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The Euclidean Steinitz–Bergström theorem

OpenAI · September 24, 2026

Every prescribed-order finite sequence of vectors in the Euclidean unit ball of ℝ^d has one signing for which every signed prefix has norm at most \(C\sqrt d\), with C absolute and independent of the sequence length. Consequently, every indexed zero-sum family of unit-ball vectors admits an ordering with the same bound for its unsigned partial sums. This determines the Euclidean Steinitz constant up to absolute factors, \(S_2(d)=\Theta(\sqrt d)\), and resolves the Euclidean Steinitz–Bergström conjecture.

Read PDF Download Source

Cite

@misc{OAI:The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026,
  author = {{OpenAI}},
  title = {{The Euclidean Steinitz--Bergstr{\"o}m theorem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf}{OAI:The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The Euclidean Steinitz–Bergström theorem

Scope

The formalized result gives the Euclidean Steinitz–Bergström bound with one absolute constant \(C\). For every finite family of vectors in the unit ball of \(\mathbb R^d\), signs can be chosen so that every prefix in the prescribed order has norm at most \(C\sqrt d\). When the vector sum is zero, a permutation makes every unsigned prefix satisfy the same bound. Repeated and zero vectors are included. The result is existential and does not supply an online algorithm.

Comparator links

Result	Comparator statement
Euclidean signed and reordered prefix bounds	SteinitzBergstrom.lean

Scope note on GitHub →