Sharp projection-body inequalities and a counterexample to simplex maximization

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Petty’s projection-volume conjecture in dimensions at least four

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026,
  author = {{OpenAI}},
  title = {{Petty's projection-volume conjecture in dimensions at least four}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026/paper.pdf}{OAI:Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026}},
  year = {2026}
}

A product counterexample to the simplex maximum for projection-body volume

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026,
  author = {{OpenAI}},
  title = {{A product counterexample to the simplex maximum for projection-body volume}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026/paper.pdf}{OAI:A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Petty's projection-volume conjecture predicts

\(\displaystyle \frac{|\Pi K|}{|K|^{n-1}}\ge \kappa_{n-1}^{n}\kappa_n^{2-n},\)

with equality exactly for ellipsoids; here \(\kappa_j\) is the volume of the Euclidean unit ball in dimension \(j\). The formalization establishes this for every convex body \(K\subset\mathbb R^n\) and every \(n\ge4\).

Other inequalities in the projection-body family are not included.

Brannen's simplex-maximization conjecture predicts that a simplex maximizes normalized projection-body volume \(|\Pi K|/|K|^{n-1}\) in dimension \(n\). The formalized counterexample is the product of two ten-dimensional simplices. Its normalized projection volume, divided by that of a twenty-dimensional simplex, is

\(\displaystyle \frac{22{,}355{,}476}{22{,}020{,}096}>1.\)

Thus the proposed maximum fails in dimension \(20\). The paper's exponential-factor result for every sufficiently large dimension is not included.

Comparator links

Result	Comparator statement
Petty's projection-volume inequality	PettyProjectionVolume.lean
Failure of the simplex upper bound in dimension 20	ProjectionCounterexample.lean
Explicit product-of-simplices counterexample	ProjectionVolume.lean

Scope note on GitHub →