Lean formalization in OpenAI math repository (Result 097)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Euclidean Steinitz–Bergström theorem'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 097). The Lean development was not rebuilt locally.