Oct 6, 2026
Lean formalization in OpenAI math repository (Result 096)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Gaussian propeller bound in every dimension'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 096). The Lean development was not rebuilt locally.