Proves that the sum of squared Gaussian first moments of any finite measurable partition is at most 9/(8\pi). In dimension at least two, three planar sectors of angle 2\pi/3, extended orthogonally, attain the bound. Combined with the separate Unique Games theorem, this proves NP-hardness of improving the loss factor (8\pi/9)(1-1/k) for identity-target kernel clustering with fixed k ≥ 3 on rational centered positive semidefinite inputs. (Lean)
Manuscript
The Gaussian propeller bound in every dimension
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026}
We prove the Gaussian propeller conjecture: for every finite measurable partition of a Euclidean space, the sum of the squared lengths of its Gaussian first moments is at most 9/(8\pi). For dimension at least two and at least three cells, three planar sectors of angle 2\pi/3, extended by an orthogonal Euclidean factor, attain the bound.
Result 096 · Convex and metric geometry. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md