Heilman simplifies OpenAI’s propeller conjecture proof
Result confirmed
The takeaway
OpenAI’s 6 Oct release contained a Lean-formalized proof of the Gaussian propeller conjecture (Khot–Naor 2008) in every dimension, a claim our dataset had missed. On 23 Oct Steven Heilman (USC), co-author of the 2012 three-dimensional case, posted a shorter version that also settles the equality cases and removes the computer search from the 3D step. It is the first expert follow-up to treat the conjecture as proved.
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 26 October 2026
Your AI and this story
- GPT-6 Astra176 days after its cutoff
- Claude Opus 5.5115 days after its cutoff
- Gemini 4 Argon206 days after its cutoff
- Grok 4.7145 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 115 days before it.
Key facts
- Abstract (verbatim): ‘We simplify and improve OpenAI’s proof of the propeller conjecture of Khot and Naor from 2008: the sum of the squared lengths of the Gaussian moments of any partition of Euclidean space is at most 9/(8π). We show equality only occurs for three 120 degree sectors in the plane … We also remove computer assistance from the three-dimensional case of the conjecture, which previously used an epsilon net traversal.’
- AI statement (verbatim): ‘GPT 6 was used to prepare this manuscript, which is based upon the solution of the Propeller Conjecture from [Ope26]. Before the release of [Ope26], we had a somewhat different proof of Theorem 1.1 that was longer and instead relied on the Gaussian isoperimetric inequality and a second variation argument.’
- Structure: proves C₄ = 9/(8π) without computer assistance, then, ‘as in [Ope26]’, shows C_N = C₄ for all N > 4
- OpenAI family 096 (catalogue): ‘The Gaussian propeller conjecture in every dimension … Combined with the separate Unique Games theorem, this proves NP-hardness of improving the loss factor (8π/9)(1−1/k) for identity-target kernel clustering with fixed k ≥ 3’; manuscript ‘The Gaussian propeller bound in every dimension’ dated 24 Sept 2026; Lean comparator challenge GaussianPropeller (theorem OAI.GaussianPropeller.all_partitions, standard axioms only)
- Prior human work: Khot–Naor (2008, 2013) posed it; Heilman, Jagannath and Naor proved the three-dimensional case (2012) with a computer-assisted ε-net step
- Heilman also says that, since the conjecture ‘is now proven’, the kernel clustering hardness of Khot–Naor needs only the Unique Games assumption, which OpenAI’s family 102 also claims to prove
What happened
OpenAI’s release of 6 Oct has 372 families, and the propeller conjecture (family 096) was not among the claims we had covered. The conjecture comes from Khot and Naor’s study of kernel clustering. Among all ways to cut Gaussian space into pieces, it asks which maximises the summed squared “centre of mass” of the pieces. The answer, 9/(8π), comes from a planar three-bladed propeller.
Steven Heilman of USC proved the three-dimensional case in 2012 with Aukosh Jagannath and Assaf Naor, partly by computer search. His 23 Oct paper takes OpenAI’s proof as its starting point, writes it out more simply, adds the characterisation of equality cases, and replaces the old computer search with a short argument. He says he had a longer proof of his own before OpenAI’s release.
Why it matters
It is one of the clearest cases so far of an expert on a problem endorsing an OpenAI release result by reproving it. Combined with OpenAI’s claimed Unique Games proof, it would settle the approximability of kernel clustering.
Sources
3 sources from 2 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
Changes
- Filed (arXiv PDF and OpenAI catalogue read)