∑math20

Convex and metric geometry · Result 087

The Mahler conjectures, functional inequalities and polar-product symplectic width

3 papersLeanreasoning

Resolves the symmetric and nonsymmetric geometric Mahler conjectures in every dimension, with Hanner polytopes and simplices as the respective volume-product minimizers and all equality cases classified. The corresponding sharp functional Mahler inequalities also hold. For n ≥ 2, every symmetric polar product \(K\times K^\circ\) in dimension \(2n\) has Gromov width 4.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 3

First page of The symmetric Mahler conjecture and its equality cases

The symmetric Mahler conjecture and its equality cases

OpenAI · September 22, 2026

We resolve the symmetric Mahler conjecture positively, including its equality classification. Every origin-symmetric convex body in ℝn has volume product at least \(4^n/n!\), with equality exactly for invertible linear images of Hanner polytopes.

Read PDF Download Source

Cite
@misc{OAI:The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026,
  author = {{OpenAI}},
  title = {{The symmetric Mahler conjecture and its equality cases}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf}{OAI:The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026}},
  year = {2026}
}
First page of The Mahler Conjecture for General Convex Bodies

The Mahler Conjecture for General Convex Bodies

OpenAI · September 22, 2026

We resolve the Mahler conjecture for general convex bodies positively. For every convex body \(K\subset\mathbb R^n\), n ≥ 1, with Santaló point \(s(K)\), \(|K|\,|(K-s(K))^\circ|\ge (n+1)^{n+1}/(n!)^2\), with equality exactly for simplices.

Read PDF Download Source

Cite
@misc{OAI:The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026,
  author = {{OpenAI}},
  title = {{The Mahler Conjecture for General Convex Bodies}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/paper.pdf}{OAI:The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026}},
  year = {2026}
}
First page of Symplectic Balls in Symmetric Polar Products

Symplectic Balls in Symmetric Polar Products

OpenAI · September 22, 2026

For every integer n ≥ 2 and every origin-symmetric convex body \(K\subset\mathbb R^n\), we prove that the Gromov width of \(\mathop{\mathrm{int}}\nolimits K\times\mathop{\mathrm{int}}\nolimits K^\circ\) is 4. We construct smooth symplectic embeddings of standard balls of every capacity \(0\lt c\lt 4\) into this polar product. Volume preservation then resolves the symmetric Mahler conjecture positively in every dimension.

Read PDF Download Source

Cite
@misc{OAI:Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026,
  author = {{OpenAI}},
  title = {{Symplectic Balls in Symmetric Polar Products}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026/paper.pdf}{OAI:Symplectic-Balls-in-Symmetric-Polar-Products-September-22-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

The symmetric Mahler conjecture predicts \(|K||K^\circ|\ge4^n/n!\) for every origin-symmetric convex body \(K\subset\mathbb R^n\). The formalization establishes this for every \(n\ge1\) and characterizes equality exactly by invertible linear images of Hanner bodies, built from intervals using Cartesian products and convex-hull joins.

The nonsymmetric Mahler conjecture and the functional inequalities are not included.

The general Mahler conjecture gives a sharp lower bound for the volume product of a convex body and its polar. For every \(n\ge1\) and compact convex body \(K\subset\mathbb R^n\) with nonempty interior, the formalization proves \(\inf_{z\in\mathrm{int}\,K}|K|\,|(K-z)^\circ|\ge (n+1)^{n+1}/(n!)^2\). Equality holds exactly when \(K\) is a simplex. The paper's functional inequality is outside this selected statement.

For an origin-symmetric convex body \(K\subset\mathbb R^n\), \(n\ge2\), the formalized result determines the symplectic ball capacity of \(\mathrm{int}\,K\times\mathrm{int}\,K^\circ\): its Gromov width is \(4\), and every ball of capacity \(0<c<4\) embeds symplectically into it. The normalization assigns capacity \(\pi r^2\) to a ball of radius \(r\).

No boundary smoothness or strict convexity is assumed. An embedding at capacity exactly \(4\) is not asserted.

Comparator links

ResultComparator statement
Symmetric Mahler inequalityMahlerConjecture.lean
Symmetric Mahler equality characterizationSymmetricMahlerEquality.lean
General Mahler inequality and simplex equality casesGeneralMahler.lean
Gromov width of symmetric polar productsSymmetricPolar.lean

Scope note on GitHub →

Reasoning summary

OpenAI released an abridged summary of the model's reasoning for this result: Symmetric and general Mahler conjectures (PDF).