---
id: "2026-10-23-propeller-conjecture-openai-proof-heilman-simplification"
url: "https://postcutoff.com/e/2026-10-23-propeller-conjecture-openai-proof-heilman-simplification/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-23"
date_precision: day
category: science
importance: 3
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: "2026-10-27"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-23-propeller-conjecture-openai-proof-heilman-simplification/

# Heilman simplifies OpenAI's propeller conjecture proof

Full title: Khot–Naor propeller conjecture: Steven Heilman, who proved the 3D case in 2012, simplifies OpenAI's proof and removes its computer assistance

The propeller conjecture of Subhash Khot and Assaf Naor (2008) says the sum of squared lengths of the Gaussian moments of the parts of any partition of Euclidean space is at most 9/(8π), attained by three 120° sectors. It gives the sharp hardness-of-approximation constant for kernel clustering under the Unique Games Conjecture. OpenAI's 6 Oct 2026 release (family 096) claims it in every dimension with a Lean comparator statement. In arXiv 2610.32158 (23 Oct) Steven Heilman "simplif[ies] and improve[s] OpenAI's proof". He shows equality only for the propeller and gives a computer-free proof of the case of four parts, which in 2012 used an ε-net search. GPT-6 helped prepare the manuscript.

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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 176 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 115 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 206 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 145 days after its cutoff

## Sources

1. [arXiv 2610.32158: On the Propeller Conjecture (Steven Heilman)](https://arxiv.org/abs/2610.32158) (arxiv.org, paper)
2. [OpenAI math catalogue (family 096: The Gaussian propeller conjecture in every dimension)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, paper)
3. [OpenAI Lean comparator challenge: GaussianPropeller](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/GaussianPropeller.lean) (github.com, code)

## Changes

- 2026-10-26 (filed): Created (arXiv PDF and OpenAI catalogue read)

## Related

- 2026-10-26: [AI-assisted results in the 26 Oct 2026 sweep](https://postcutoff.com/e/2026-10-26-ai-assisted-results-october-26-listing/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [OpenAI model claims a proof of Khot's Unique Games Conjecture, with Lean formalization](https://postcutoff.com/e/2026-10-06-unique-games-conjecture-openai/index.md)