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

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 3

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 ℝⁿ 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}
}

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}
}

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

Result	Comparator statement
Symmetric Mahler inequality	MahlerConjecture.lean
Symmetric Mahler equality characterization	SymmetricMahlerEquality.lean
General Mahler inequality and simplex equality cases	GeneralMahler.lean
Gromov width of symmetric polar products	SymmetricPolar.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).