Proves Petty's projection-volume conjecture in the remaining dimensions n ≥ 4: ellipsoids uniquely minimize projection-body volume at fixed body volume. Also establishes the full Lutwak–Petty projection inequalities. In contrast, products of simplices exceed Brannen's proposed simplex maximum for normalized projection-body volume by an exponential factor in every sufficiently large dimension. (Lean)
Manuscripts (2)
Petty’s projection-volume conjecture in dimensions at least four
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026}
We prove that ellipsoids uniquely minimize the volume of the projection body among convex bodies of fixed volume in every dimension at least four. This proves Petty's projection-volume conjecture in these dimensions.
A product counterexample to the simplex maximum for projection-body volume
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026}
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.
Result 088 · Convex and metric geometry. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md