Episode 087, October 2026

Mahler, solved?

The smallest volume products of convex bodies, and symplectic balls in polar products

Covers result 087 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.

Play Episode 087: Mahler, solved? A yellow wireframe cube beside a pink wireframe octahedron, its polar, and a teal triangle inside its larger pink polar triangle, above the inequality: the volume of K times the volume of its polar is at least 4 to the n over n factorial.

7:52. English captions available. The video loads from YouTube when you press play.

Chapters

The claims, in plain words

The polar of a convex body K symmetric about the origin is K° = {y : ⟨x, y⟩ ≤ 1 for every x in K}. A large body has a small polar, and the volume product |K| |K°| does not change under invertible linear maps. In the plane a disk gives π² ≈ 9.87, a regular hexagon 9 and a square 8. Ellipsoids give the largest value (the Blaschke–Santaló inequality). In the late 1930s Mahler asked for the smallest; the conjectured answer in n dimensions is 4ⁿ/n!, the value of a cube and its polar cross-polytope, shared by all Hanner polytopes, built from intervals by products and by convex hulls of copies in complementary directions. Mahler proved the plane inequality, Reisner showed that only parallelograms attain it, and Iriyeh and Shibata proved dimension three in 2020; Saint-Raymond (unconditional bodies) and Reisner (zonoids) settled special classes, and Bourgain and Milman proved the bound up to a factor exponential in the dimension.

Without symmetry, one minimizes over the position of the origin (the minimizer is the Santaló point), and the conjectured minimum is (n + 1)ⁿ⁺¹/(n!)², attained by simplices: 27/4 = 6.75 for a triangle, 64/9 ≈ 7.11 for a tetrahedron. Mahler and Meyer settled the plane, Meyer and Reisner polytopes with at most n + 3 vertices, and a 2026 preprint of Chen, Li, Xi and Xu treats dimension three. From symplectic geometry, Artstein-Avidan, Karasev and Ostrover showed in 2014 that a conjecture of Viterbo would imply the symmetric Mahler conjecture.

Result 087 is three OpenAI preprints, all dated September 22, 2026. The first (26 pages) proves |K| |K°| ≥ 4ⁿ/n! for every origin-symmetric convex body in every dimension, with equality exactly for linear images of Hanner polytopes. The second (72 pages) proves that the product at the Santaló point is at least (n + 1)ⁿ⁺¹/(n!)², with equality exactly for simplices. Both derive sharp functional versions for log-concave functions and their convex conjugates, with constants 4ⁿ for even functions and eⁿ in general. The third (19 pages) puts K in the position coordinates and K° in the momentum coordinates of phase space and proves, for n ≥ 2, that standard symplectic balls of every capacity below 4 fit inside and none larger: the Gromov width is 4. Since a ball of capacity 4 has volume 4ⁿ/n! and symplectic maps preserve volume, this proves the symmetric inequality a second time, without the equality cases.

What it doesn’t claim

Viterbo’s broader conjecture is false in general, as Haim-Kislev and Ostrover showed, and the papers claim nothing about it beyond these polar products. An embedding of a ball of capacity exactly 4 is not claimed. The symplectic route gives no equality cases.

Where it stands

Posted as preprints: OpenAI, three papers dated September 22, 2026, released October 6
Peer reviewed: Not yet
Checked in Lean: OpenAI published Lean proofs of the three main theorems; we have not run the checks

Last checked October 19, 2026. None of the preprints has been revised. OpenAI published Lean formalizations of the three main theorems, with no unproved steps that we could find: 243 files and 28,853 lines for the symmetric inequality and its equality cases, 302 files and 40,205 lines for the general inequality and its simplex equality, and 46 files and 12,175 lines for the symplectic width, matched against four separate statements (symmetric inequality, symmetric equality, general inequality and equality, Gromov width). The functional inequalities, which rest on earlier implications of Fradelizi and Meyer, are not formalized. We have not run the checks. The symmetric paper says its argument is independent of the general one, and the symplectic paper uses neither. None of the papers is among those OSVerify reviewed, and we have seen no expert review.

How the proofs go

Symmetric: a conformal lens. A conformal map from the disk onto a lens-shaped region turns uniform angles on the circle into a uniform vertical coordinate; it is a rotation of a map Gross used for a conformal Skorokhod embedding. For a body cut out by finitely many symmetric strips, random boundary angles determine complex points, and a mass estimate at an isolated holomorphic zero, proved with Stokes’ theorem, shows that certain probabilities add up to at least one. An exact identity turns that sum into an integral, over the body, of the volume covered by certain simplices inside the polar body, which gives the bound. For equality, every triple of points in the norm whose unit ball is the polar body has a metric median, and a classification of Hansen and Lima gives the Hanner polytopes.
General: Gaussian projections onto cones. Klartag’s correspondence between a body and a pair of dual cones turns the volume product into a product of Laplace integrals. Gaussian vectors projected onto the two cones, with a carefully chosen bias and covariance, give maps into the cones, and their Jacobians with Jensen’s inequality reduce everything to showing that an error term is at most zero. The derivative matrices need not commute, so the paper compares them with spectral thresholds of a linear Gaussian matrix, using Hermite expansions and divided differences. Its scalar inequalities are proved with finite rational certificates, plus interpolation and tail estimates, and supplementary programs check them. Equality forces the matrices to commute, so the cone splits into half-lines and the body is a simplex.
Symplectic: balls from holomorphic vanishing. If holomorphic functions vanish to order k at a single common zero, the region where their squared sizes add up to less than one, with a symplectic form built from those functions, contains balls of every capacity below πk. Using powers of the inverse lens map, the paper maps that region into the body times a polar scaled by about πk/4; dividing out leaves balls of every capacity below 4. A supporting cylinder and Gromov’s nonsqueezing theorem give the matching upper bound.

The numbers in the video

A short Python script computes volume products: π² ≈ 9.87 for a disk, 9 for a regular hexagon, 8 for a square, 27/4 = 6.75 for a triangle at its Santaló point and 64/9 ≈ 7.11 for a tetrahedron. The cube, the cross-polytope and the prism over an octahedron give exactly 4ⁿ/n!.
Among random origin-symmetric polytopes with at least 2n + 2 vertices, the smallest products found were 8.0003, 10.6746 and 10.6707 in dimensions 2, 3 and 4 (the conjectured minima are 8, 10.6667 and 10.6667). Among random general polytopes minimized over the center, the smallest were 6.7533 and 7.2706 in dimensions 2 and 3 (against 6.75 and 7.1111). No computation can test every body.

Read the source

The symmetric Mahler conjecture and its equality cases (PDF), 26 pages.
The Mahler Conjecture for General Convex Bodies (PDF), 72 pages, and its verification programs.
Symplectic Balls in Symmetric Polar Products (PDF), 19 pages.
The Lean scope note.
The collection’s catalog, where this is result 087.

The 3 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.

The symmetric Mahler conjecture and its equality cases main paper
The Mahler Conjecture for General Convex Bodies companion
Symplectic Balls in Symmetric Polar Products companion

Transcript

Read the full script

0:00The smallest product

Take a convex body that is symmetric about the origin, and form its polar: all points whose dot product with every point of the body is at most one. A large body has a small polar, and the product of their volumes does not change under any invertible linear map. In the plane, a disk gives π², about 9.87; a regular hexagon gives nine; a square gives eight. The largest value belongs to ellipses and ellipsoids, by the Blaschke–Santaló inequality. In the late 1930s, Mahler asked for the smallest, and the conjectured answer in n dimensions is 4ⁿ/n!: the value of a cube and its polar, the cross-polytope. The cube is not alone. Hanner polytopes, built from intervals by taking products and by taking convex hulls of copies placed in complementary directions, all give the same value. Up to linear maps, in three dimensions these are the cube and the octahedron; from four dimensions on, mixed ones appear, like a prism over an octahedron. In our computation the cube, the cross-polytope and the prism over an octahedron each give exactly 4ⁿ/n!, and among thousands of random symmetric polytopes in dimensions two, three and four, none went lower; the closest came within 0.1%. Mahler proved the plane inequality, Reisner later showed that only parallelograms attain it, and Iriyeh and Shibata proved dimension three in 2020. Special classes, such as Saint-Raymond’s unconditional bodies and Reisner’s zonoids, were settled earlier, and Bourgain and Milman proved the bound up to a factor exponential in the dimension. Without symmetry, the polar depends on where the origin sits, so one takes the point that makes the product smallest, the Santaló point. The conjectured minimum is then (n + 1)ⁿ⁺¹/(n!)², attained by simplices: 6.75 for a triangle, and about 7.11 for a tetrahedron. Our random searches stayed above both, at about 6.753 and 7.27. Mahler and Meyer settled the plane, Meyer and Reisner handled polytopes with few vertices, and a 2026 preprint of Chen, Li, Xi and Xu treats dimension three. A third thread comes from symplectic geometry: Artstein-Avidan, Karasev and Ostrover showed in 2014 that a conjecture of Viterbo would imply the symmetric Mahler conjecture.

2:33The claims

Result 087 is three OpenAI preprints, all dated September 22. The first, 26 pages, proves the symmetric conjecture in every dimension: every origin-symmetric convex body has volume product at least 4ⁿ/n!, with equality exactly for linear images of Hanner polytopes. The second, 72 pages, proves the general conjecture: at the Santaló point the product is at least (n + 1)ⁿ⁺¹/(n!)², with equality exactly for simplices. Both papers also derive sharp functional versions, for log-concave functions and their convex conjugates, with constants 4ⁿ for even functions and eⁿ in general. The third, 19 pages, works in phase space. Put the body in the position coordinates and its polar in the momentum coordinates. For bodies of dimension at least two, the paper proves that standard symplectic balls of every capacity below four fit inside, and none larger: the Gromov width is four. A ball of capacity four has volume 4ⁿ/n!, and symplectic maps preserve volume, so this proves the symmetric inequality a second time, without the equality cases. OpenAI published Lean formalizations of all three main theorems: about 29,000 lines for the symmetric inequality and its equality cases, 40,000 for the general inequality and its simplex equality, and 12,000 for the symplectic width, checked against four separate comparator statements, two of them for the symmetric paper. The functional inequalities are not formalized. We have not run the checks.

4:20Three proofs

The symmetric proof is complex-analytic. It uses a conformal map from the disk onto a lens-shaped region, chosen so that uniform angles on the circle become a uniform vertical coordinate, a rotation of a map Gross used for a conformal Skorokhod embedding. For a body cut out by finitely many symmetric strips, random boundary angles determine complex points, and a mass estimate at an isolated holomorphic zero, proved with Stokes’ theorem, shows that certain probabilities add up to at least one. An exact identity turns that sum into an integral, over the body, of the volume covered by certain simplices inside the polar body, which gives the bound. For equality, every triple of points in the norm whose unit ball is the polar body turns out to have a metric median, and a classification of Hansen and Lima then gives the Hanner polytopes. The general proof starts from Klartag’s correspondence between a body and a pair of dual cones, which turns the volume product into a product of Laplace integrals. Gaussian vectors, projected onto the two cones with a carefully chosen bias and covariance, give maps into the cones, and their Jacobians with Jensen’s inequality reduce everything to showing that an error term is at most zero. The derivative matrices need not commute, so the paper compares them with spectral thresholds of a linear Gaussian matrix, using Hermite expansions and divided differences. Its scalar inequalities are proved with finite rational certificates, plus interpolation and tail estimates, and supplementary programs check them. Equality forces the matrices to commute, so the cone splits into half-lines and the body is a simplex. The symplectic proof turns holomorphic vanishing into balls. If holomorphic functions vanish to order k at a single common zero, the region where their squared sizes add up to less than one, given a symplectic form built from those functions, contains balls of every capacity below πk. Using the inverse of the same lens map, raised to the k-th power, the paper maps that region into the body times a rescaled polar, with scale about πk/4; dividing out leaves balls of every capacity below four. Gromov’s nonsqueezing theorem, with a supporting cylinder, gives the matching upper bound.

6:46Where it stands

None of the three preprints is peer reviewed, and none has been revised. OpenAI’s Lean formalizations cover the symmetric inequality and its equality cases, the general inequality and its simplex equality, and the symplectic width; we have not run them. The functional inequalities rest on earlier implications of Fradelizi and Meyer, and are not formalized. The symmetric paper says its argument is independent of the general one, and the symplectic paper uses neither. None of the papers is among those OSVerify reviewed, and we have seen no expert review. If they hold, Mahler’s questions are answered in every dimension: cubes, cross-polytopes and the other Hanner polytopes minimize the symmetric volume product, and simplices minimize the general one. Viterbo’s broader conjecture is false in general, as Haim-Kislev and Ostrover showed, and these papers claim nothing about it beyond these polar products. An embedding of a ball of capacity exactly four is not claimed.

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.