Smallest shadows?
Petty’s projection-volume conjecture, and a counterexample to the simplex maximum
Covers result 088 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
6:18. English captions available. The video loads from YouTube when you press play.
Chapters
The claims, in plain words
Shine a light on a convex body from every direction and record the area of its shadow. Those areas define a second convex body, the projection body ΠK: how far it reaches from its center in each direction is the area of the shadow cast by light shining in that direction. The ratio |ΠK|/|K|n−1, where n is the dimension, does not change under affine maps. In three dimensions a ball gives about 7.40, a cube 8, a regular octahedron 9 and a tetrahedron 18.
In 1971 Petty conjectured that, in every dimension from three on, ellipsoids give the smallest value, and only ellipsoids. (A related inequality of Petty for the polar of the projection body was already known.) Lutwak reformulated the conjecture; Saroglou and Zvavitch, and Ivaki, proved local versions near the ball; Mielke-Sulz treated bodies of revolution; and a 2026 preprint of Chen, Feng, Li, Xi and Xu proved dimension three. In 1996 Brannen conjectured that simplices give the largest value. In dimension three that is true, by the same preprint, but a 2026 preprint of Feng, Hu, Liu and Xu found counterexamples in every dimension from nine on.
Result 088 is two OpenAI preprints dated September 24, 2026. The first (30 pages) proves Petty’s conjecture in every dimension n ≥ 4: for every convex body, |ΠK|/|K|n−1 ≥ κn−1n κn2−n, the ellipsoid value, with equality exactly for ellipsoids. Together with the three-dimensional preprint the conjecture would hold for every n ≥ 3, and the paper derives the Lutwak–Petty lower-degree projection inequalities, a sharp affine Sobolev-type inequality, and Holmes–Thompson isoperimetry in normed spaces. The second (7 pages) shows that the product of two ten-dimensional simplices beats the twenty-dimensional simplex by the factor 22,355,476/22,020,096, about 1.5%, and that repeating ten-dimensional factors makes the excess grow exponentially with the dimension.
What it doesn’t claim
In dimension four and up, the largest value of the ratio, and which bodies attain it, are not determined. The three-dimensional case of Petty’s conjecture is a separate preprint, not this one.
Where it stands
- Posted as preprints
- OpenAI, two papers dated September 24, 2026, released October 6
- Peer reviewed
- Not yet
- Checked in Lean
- OpenAI published Lean proofs of Petty’s inequality (n ≥ 4) and the dimension-20 counterexample; we have not run the checks
Last checked October 19, 2026. Neither preprint has been revised. OpenAI published Lean formalizations: Petty’s inequality and its equality case for every n ≥ 4 (33 files, 13,670 lines, matched against a separate statement), and the dimension-20 counterexample in two versions (the failure of the simplex bound and the exact ratio), with no unproved steps that we could find. The consequences and the exponential excess are not formalized. We have not run the checks. The statement for every dimension from three on, and its consequences as stated from dimension three on, also rely on the separate three-dimensional preprint. Brannen’s bound had already failed in dimensions nine and up; the counterexample paper’s contribution is the product construction, its exact value, and the exponential growth of the excess. Neither paper is among those OSVerify reviewed, and we have seen no expert review.
How the proofs go
- A measure on vectors. After normalizing the volume, the first variation of volume gives a probability measure on vectors: integrating the support function of any symmetric body against it gives at least a root of that body’s volume. The same measure represents the projection body through the absolute dot product. The core theorem bounds from below the double integral of the absolute dot product for any two measures with that property; applied to the body and its rescaled projection body, it gives the inequality.
- Spherical harmonics and affine position. A new inequality bounds the higher harmonics of a power of any norm by a difference of its spherical means, strictly unless the norm is Euclidean. A sign test bounds the pairing by a bilinear form in the cosine and Funk transforms, and the norm estimate controls every harmonic of degree four and up. The degree-two part is removed by choosing affine coordinates: a family of variational minimizers is extended continuously to singular matrices, an inward-pointing field appears at the boundary, and Brouwer’s fixed-point theorem gives the position. Equality then forces an ellipsoid.
- The product counterexample. For a polytope, the projection body is a sum of segments, one for each facet, of length its area. For a product of two polytopes the facets split into two families, and the ratio multiplies. A simplex in dimension d gives (d + 1)dd/d!, and the value for ten, squared, exceeds the value for twenty.
The numbers in the video
- A short Python script computes projection bodies of polytopes as sums of facet segments. In dimension 3 the ratio is 7.40 for a ball, 8 for a cube, 9 for a regular octahedron and 18 for a tetrahedron; in dimension 4, 12.64, 16, 20 and 53.33. Hulls of 20, 60, 180 and 540 random points on the sphere give 9.68, 8.07, 7.64 and 7.48, approaching the ball. 600 random polytopes in dimension 3 and 200 in dimension 4 all lie between the ball and simplex values.
- The product rule checks numerically, the exact ratio for two ten-dimensional simplices is 22,355,476/22,020,096 ≈ 1.0152, and among products of two simplices (both of dimension at least two), dimension 20 is the first where one beats the simplex. No computation can test every body.
Read the source
- Petty’s projection-volume conjecture in dimensions at least four (PDF), 30 pages.
- A product counterexample to the simplex maximum for projection-body volume (PDF), 7 pages.
- The Lean scope note.
- The collection’s catalog, where this is result 088.
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00Shadows of a body
Shine a light on a convex body from every direction, and record the area of its shadow. Those shadow areas, one for each direction, define a second convex body, the projection body: how far it reaches from its center in each direction is the area of the shadow cast by light shining in that direction. Divide the volume of the projection body by the volume of the original body to the power n − 1, where n is the dimension, and the result does not change under stretching, shearing or moving the body. In three dimensions, a ball gives about 7.4, a cube eight, a regular octahedron nine, and a tetrahedron eighteen. In 1971, Petty conjectured that in every dimension from three on, ellipsoids give the smallest value, and only ellipsoids. A related inequality for the polar of the projection body, also due to Petty, was already known. Lutwak reformulated the conjecture as a lower bound for an integral of the absolute dot product against surface-area measures. Saroglou and Zvavitch, and Ivaki, proved local versions near the ball; Mielke-Sulz handled bodies of revolution; and a 2026 preprint of Chen, Feng, Li, Xi and Xu proved dimension three. In our computation, hulls of more and more random points on a sphere come down toward the ball’s value, from 9.68 with 20 points to 7.48 with 540. The opposite question is the largest value. In 1996, Brannen conjectured that simplices give the maximum. In dimension three that is true, by the same group’s preprint, and none of our hundreds of random polytopes in dimensions three and four went above the simplex. But a 2026 preprint of Feng, Hu, Liu and Xu found counterexamples in every dimension from nine on, built from perturbed projections of a cube.
1:55The claims
Result 088 is two OpenAI preprints, both dated September 24. The first, 30 pages, proves Petty’s conjecture in every dimension from four on: for every convex body, the normalized projection volume is at least the ellipsoid value, with equality exactly for ellipsoids. Together with the separate three-dimensional preprint, the conjecture would then hold in every dimension from three on, and the paper derives consequences: the Lutwak–Petty lower-degree projection inequalities, a sharp affine Sobolev-type inequality, and an isoperimetric inequality for the Holmes–Thompson area in normed spaces. The second, 7 pages, gives an explicit counterexample to Brannen’s bound: the product of two ten-dimensional simplices, in dimension twenty, beats the twenty-dimensional simplex by a factor of 22,355,476/22,020,096, about 1.5%. Repeating ten-dimensional factors, the excess grows exponentially with the dimension. OpenAI published Lean formalizations of Petty’s inequality with its equality case for every dimension from four on, about 14,000 lines, and of the dimension-twenty counterexample, in two separate versions. The consequences and the exponential excess are not formalized. We have not run the checks.
3:23How the proofs go
The proof of Petty’s conjecture turns a body into a measure on vectors. After normalizing the volume, the first variation of volume gives a probability measure: integrating the support function of any symmetric body against it gives at least a root of that body’s volume. The same measure represents the projection body through the absolute dot product. The core theorem bounds from below the double integral of the absolute dot product for any two measures with that property. Applied to the body and its rescaled projection body, it gives the inequality. The estimate runs through spherical harmonics. A new inequality bounds the higher harmonics of a power of any norm by a difference of its spherical means, strictly unless the norm is Euclidean. A sign test bounds the pairing by a bilinear form in the cosine and Funk transforms, and the new norm estimate controls every harmonic of degree four and up. The degree-two part is removed by choosing affine coordinates: the paper extends a family of variational minimizers continuously to singular matrices, finds an inward-pointing field at the boundary, and uses Brouwer’s fixed-point theorem. Equality then forces an ellipsoid. The counterexample is short. For a polytope, the projection body is a sum of segments, one for each facet, of length its area. For a product of two polytopes, the facets split into two families, and the normalized projection volume multiplies: the value of a product is the product of the values. A simplex in dimension d gives (d + 1)·dᵈ/d!. Two ten-dimensional simplices give that value for ten, squared, which exceeds the value for twenty. In our scan, twenty is the first dimension where any product of two simplices wins.
5:16Where it stands
Neither preprint is peer reviewed, and neither has been revised. OpenAI’s Lean formalizations cover Petty’s inequality and its equality case from dimension four on, and the dimension-twenty counterexample; we have not run them. The statement for every dimension from three on, and its consequences as stated from dimension three on, also rely on the separate three-dimensional preprint. Brannen’s bound had already failed in dimensions nine and up in Feng, Hu, Liu and Xu’s preprint; this paper’s contribution there is the product construction, its exact value, and the exponential growth of the excess. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If they hold, ellipsoids are exactly the bodies with the smallest normalized projection volume in every dimension from four on. In dimension four and up, the largest value, and which bodies attain it, are not determined.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.