∑math20

Convex and metric geometry · Result 096

The Gaussian propeller conjecture in every dimension

1 paperLean

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.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of The Gaussian propeller bound in every dimension

The Gaussian propeller bound in every dimension

OpenAI · 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.

Read PDF Download Source

Cite
@misc{OAI:The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026,
  author = {{OpenAI}},
  title = {{The Gaussian propeller bound in every dimension}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf}{OAI:The-Gaussian-Propeller-Bound-in-Every-Dimension-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):

Scope

The Gaussian propeller problem asks how large the sum of squared Gaussian first moments can be over a partition. The formalized result proves the sharp bound \(9/(8\pi)\) for every positive dimension and every positive number of labelled cells, allowing empty cells and arbitrary masses. In dimension at least two with at least three cells, three planar sectors of angle \(120^\circ\), extended in orthogonal directions, attain equality. The separate Gaussian-maxima and kernel-clustering consequences are not included.

Comparator links

ResultComparator statement
Gaussian propeller bound and attainmentGaussianPropeller.lean

Scope note on GitHub →