Browse › Convex and metric geometry › 096 The Gaussian propeller conjecture in every dimension
The Gaussian propeller bound in every dimension
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 096 (lean/docs/096.md, release of 2026-10-06). The scope note states that the Lean development covers the $9/(8\pi)$ bound for all $d,k\ge1$, including empty cells and arbitrary masses, and propeller attainment for $d\ge2$, $k\ge3$, but not the Gaussian-maxima corollary or the kernel-clustering consequence.
- OpenAI, GaussianPropeller/Main.lean (openai/math, 2026-10-06). This file holds the release's main Lean theorem
GaussianPropeller.all_partitions, which combines the partition bound, proved by strong induction on the number of cells, with propeller attainment; the comparator statement is inlean/ComparatorChallenges/GaussianPropeller.lean. - anxkhn, feat(Paper): add the Gaussian propeller bound (google-deepmind/formal-conjectures PR #7002, opened 2026-10-08). This PR adds an independent Lean statement of the upper bound in Theorem 1.1 to formal-conjectures, without a proof and without attainment; it was open with one approving review (bocowgill, 2026-10-10). [AI-generated per source]
- anxkhn, Add the Gaussian propeller partition bound (google-deepmind/formal-conjectures issue #6997, 2026-10-08). This issue proposes the statement scope used in PR #7002: positive dimension and cell count, a.e. partitions, empty cells allowed, and unnormalized first moments.
Related prior literature mentioned by others
- Steven Heilman, Aukosh Jagannath and Assaf Naor, Solution of the propeller conjecture in ℝ³ (Discrete & Computational Geometry 50, 263–305, 2013; arXiv:1112.2993). The course's dependency list identifies this computer-assisted three-dimensional theorem as the input handling extremizers with at most four active cells in the manuscript.
Possibly relevant literature (found by the agent, not checked)
- M. Isaksson and E. Mossel, Maximally Stable Gaussian Partitions with Discrete Applications (arXiv:0903.3362, 2009; Israel J. Math. 2012). This is the origin of the equal-measure Gaussian noise-stability partition problem that the introduction contrasts with the unrestricted first-moment functional.
- S. Heilman, Euclidean Partitions Optimizing Noise Stability (arXiv:1211.7138, 2012). Earlier work on the three-cell standard simplex conjecture, relevant to the paper's comparison with Heilman's conditional route via noise-stability maximizers.
- S. Heilman, E. Mossel and J. Neeman, Standard Simplices and Pluralities are Not the Most Noise Stable (arXiv:1403.0885, 2014). This paper shows that the simplex partition is not noise-stability optimal when cell measures are unequal, which bears on the paper's remark that its result imposes no cell-mass constraint.
- E. Milman and J. Neeman, The Gaussian Double-Bubble and Multi-Bubble Conjectures (arXiv:1805.10961, 2018; Ann. of Math. 2022). This is a related sharp Gaussian partition problem with simplicial or tripod extremal clusters, relevant to the "related partition problems" discussion in the introduction.
- Steven Heilman, Stable Gaussian minimal bubbles (Calculus of Variations and Partial Differential Equations 65, article 271, 13 October 2026). Section 1.4 studies a prescribed-mass, shifted first-moment variant of the propeller problem, related to the manuscript's distinction between its unrestricted first-moment bound and constrained Gaussian partition problems.
Digests and expositions
- Open Mathematics Courses / Claude Opus 5.5, The Gaussian propeller bound (six-lesson online course, undated). The course develops the manuscript's Gaussian-maxima duality, rearrangement and deletion estimates, residual covariance bounds and kernel-clustering application, with exercises and an explicit notice that independent review is incomplete. [AI-generated per source]
- heyprof, Gaussian propeller — the best partition of space (3D) (interactive exposition, undated). The exposition illustrates the manuscript's unnormalized Gaussian first-moment objective with adjustable sectors and several spatial partitions, distinguishing numerical examples from the claimed universal bound.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 096
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/096.md. The Lean statements have not been checked by people against the paper's claims.
Family 096: The Gaussian propeller conjecture in every dimension
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.
This is the only paper in this family.