# The Gaussian propeller conjecture in every dimension

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

- [The Gaussian propeller bound in every dimension](../../preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Gaussian propeller bound and attainment | [GaussianPropeller.lean](../ComparatorChallenges/GaussianPropeller.lean) |