Oct 6, 2026
Lean formalization in OpenAI math repository (Result 088)
Model / AI: OpenAI (unreleased)
machine-checked (counterexample)self-reported (counterexample)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A product counterexample to the simplex maximum for projection-body volume'. The product of two ten-dimensional simplices has larger normalized projection-body volume than a twenty-dimensional simplex. This gives a counterexample to Brannen's proposed simplex maximum.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 088). The Lean development was not rebuilt locally.