The Gaussian propeller conjecture
From OpenAI Aftermath
The Gaussian propeller conjecture asks for the largest possible value of the sum of the squared Gaussian first moments of the cells of a measurable partition of a Euclidean space, where the first moment of a cell A is the unnormalized vector ∫A x dγ(x) for the standard Gaussian measure γ. The conjectured answer is 9/(8π), attained by a "propeller" of three planar sectors of angle 2π/3. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the conjecture in every dimension. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; this page does not certify them.
Background
- As recounted in the introduction of the manuscript:
- The conjecture arose in Khot and Naor's study of approximate kernel clustering, where Gaussian first moments govern approximation and Unique Games hardness. Khot and Naor proved that a maximizer can be chosen to be a conical partition in the span of its centroids, and determined the value for three cells.
- Heilman, Jagannath and Naor proved the bound for every finite partition of R3, with a computer-assisted treatment of the remaining four-cell conical configurations. The manuscript uses that theorem as an input.
The original results
- Claim (the propeller bound). Theorem 1.1 of The Gaussian propeller bound in every dimension states that for all positive integers d and k, every measurable partition (A1, …, Ak) of Rd satisfies Σi ‖∫Ai x dγd(x)‖2 ≤ 9/(8π), with empty cells and arbitrary cell probabilities allowed. The bound is sharp whenever d ≥ 2 and k ≥ 3: three planar sectors of angle 2π/3, multiplied by the orthogonal complement of their plane, attain it.
- Method, as described: the manuscript reproves the needed form of Khot and Naor's reduction to conical partitions, and its new estimates show that an extremizer with five or more cells of positive measure cannot exceed 9/(8π), while Heilman, Jagannath and Naor's three-dimensional theorem is taken as an established input.
- Consequence, as summarized by the collection. The collection's contents page states that, combined with the separate Unique Games theorem, the bound gives NP-hardness of improving the loss factor (8π/9)(1 − 1/k) for identity-target kernel clustering with fixed k ≥ 3 on rational centered positive semidefinite inputs.
- Sources. At commit
1581d4c: The Gaussian propeller bound in every dimension. - Formalization, as described by the repository. The scope note lean/docs/096.md states that the Lean formalization proves the sharp bound 9/(8π) for every positive dimension and every positive number of labelled cells, allowing empty cells and arbitrary masses, together with the attainment by the propeller in dimension at least two with at least three cells, and that the Gaussian-maxima and kernel-clustering consequences are not included. The Comparator challenge is
GaussianPropeller.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 23 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit bb5fdb6, 18 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a sandboxed Comparator pass for GaussianPropeller. Its note states that the sharp bound and its attainment are stated formally, and that the NP-hardness consequence for kernel clustering is not. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | Formal Conjectures, pull request 7002 (anxkhn) | Reading (formal statement) | Adds the bound of Theorem 1.1 as a statement in the Formal Conjectures repository, for every positive dimension and positive number of labelled cells, with the cells forming a partition almost everywhere. Attainment and the clustering consequences are outside the pull request, and no formal proof is linked. | Open pull request, prepared with AI assistance. |
| 2026-10-08 | mxym/math research notes on variants of the functional: mass-constrained fans, dimension rate, quadratic dimension, spherical-cap converse and arbitrary masses | Extension (variants of the problem) | Notes that state they build on or complement the manuscript. For planar sector fans in which every cell has a prescribed minimum angle, an exact formula for the constrained maximum. For k cells of Gaussian mass 1/k, explicit partitions in dimension at most Cε log k that reach the fraction 1 − ε of the optimum over all dimensions, and partitions in dimension at most ⌈(log k)2⌉ + 1 that come within 92/k of it, each with a converse showing that the dimension order cannot be lowered. A further note gives a nonasymptotic bound for arbitrary prescribed positive masses. | Repository notes prepared with AI assistance. The READMEs describe complete analytic proofs with exact-rational checks and make no priority claim or claim of formal verification. |
| 2026-10-08; four-cell preprint 2026-10-10, revised to 2026-10-13 | Yongxian Zhang, Equal Gaussian cells: the sharp simplex first-moment theorem (mxym/math, research/gaussian-balanced-simplex-all-k); Four equal Gaussian cells: covariance deformation and tetrahedral rigidity, Zenodo 10.5281/zenodo.23272806 and aiXiv:2610.01490 (repository); companion counterexample note | Related (the equal-mass problem) | For every k ≥ 2, every partition of Rd into k cells of Gaussian mass 1/k satisfies Σi ‖∫Ci x dγd‖2 ≤ (E maxi ≤ k Zi)2/(k − 1), where the Zi are independent standard normals; for d ≥ k − 1 equality holds exactly for central regular simplex cones. The repository states that this proves the equal-mass case of Heilman's 2019 Conjecture 1.16 for every k and his 2014 Conjecture 3 in dimension three, and its companion note gives a counterexample to Conjecture 1.16 for unequal masses arbitrarily close to equal ones. The proofs use the Milman–Neeman Gaussian multi-bubble theorem. The literature note compares the result with the manuscript's bound, which does not fix the cell masses; for k = 3 the regular simplex fan is the propeller. | Zenodo and aiXiv preprint for four cells and repository manuscripts for all k, prepared with AI assistance and not peer reviewed; the reviews in the repository are internal. The four-cell README states that a Lean project checks the internal proof chain except the multi-bubble theorem and parts of the Gaussian integral evaluation. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 for GaussianPropeller | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the solution, in 634 s. | Repository. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
