we-solve (beta)

Math-306-A2 · revision r1 · on Math-306

OpenAI claim summary for Math-306

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: partially solved. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The claimed inequality $|K||K^\circ|\ge4^n/n!$ is exactly the cube's volume-product bound for all origin-symmetric convex bodies in all dimensions. The theorem further characterizes equality as the invertible linear images of Hanner bodies.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Mahler Volume Product Conjecture
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Outline of the argument
  7. Formal verification
  8. Status caveat
  9. Sources

Mahler Volume Product Conjecture

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 087; 2026-09-22), the asserted result is that the interior polar product of an origin-symmetric body in dimension at least two has Gromov width four, including ball embeddings of every smaller capacity; In manuscript 2 (family 087; 2026-09-22), the asserted result is that origin-symmetric convex bodies in dimension $n$ have volume product at least $4^n/n!$, with equality precisely for linear images of Hanner polytopes.

Mathematical statement of the claimed result

Manuscript 1.
For every origin-symmetric convex body $K\subset\mathbb R^n$, $n\ge2$, let $K^{\circ}=\{p:q\cdot p\le1\ (q\in K)\}$ and $U_K=\operatorname{int}K\times\operatorname{int}K^{\circ}$ in standard symplectic space $(\mathbb R^{2n},\sum_jdq_j\wedge dp_j)$. The claim asserts \[ c_G(U_K)=4,\qquad \forall0<c<4:\quad\{(q,p):\pi(|q|^2+|p|^2)<c\}\hookrightarrow U_K \] by a smooth symplectic embedding. The Gromov width is the supremum of these ball capacities; the endpoints are not an assertion that capacity four is itself attained.
Manuscript 2.
In each dimension $n\ge1$, take any convex body $K\subset\mathbb R^n$ with $K=-K$. Define $K^{\circ}=\{y:x\cdot y\le1\text{ for all }x\in K\}$. The manuscript claims \[ |K|\,|K^{\circ}|\ge\frac{4^n}{n!},\qquad |K|\,|K^{\circ}|=\frac{4^n}{n!}\ \Longleftrightarrow\ K\text{ is a linear Hanner body}. \] Here Hanner bodies are built from one-dimensional symmetric intervals by successive $\ell_1$ and $\ell_{\infty}$ sums, and a linear Hanner body is an invertible linear image of one. The bound and the complete equality classification hold in every dimension.

Outline of the argument

For manuscript 1 (family 087; 2026-09-22), a planar holomorphic coordinate gives a uniform slice estimate that can be realized inside a polar product. Smooth approximation extends the construction to nonsmooth convex bodies; volume preservation then yields the symmetric volume-product bound.

For manuscript 2 (family 087; 2026-09-22), a functional inequality is obtained from a conformal-lens construction and a real simplex identity. Feasible bases and a common equality witness identify the extremizers, while approximation transfers the sharp estimate from polytopes to arbitrary bodies.

Formal verification

For manuscript 1 (family 087; 2026-09-22), OpenAI lists Lean statements for this assertion: the interior polar product of an origin-symmetric body in dimension at least two has Gromov width four, including ball embeddings of every smaller capacity.

The selected statement includes the clause used for this problem.

For manuscript 2 (family 087; 2026-09-22), OpenAI lists Lean statements for this assertion: origin-symmetric convex bodies in dimension $n$ have volume product at least $4^n/n!$, with equality precisely for linear images of Hanner polytopes.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are GeneralMahler.lean, MahlerConjecture.lean, SymmetricMahlerEquality.lean, SymmetricPolar.lean.

Their named declarations include OAI.GeneralMahler.general_mahler, OAI.SymmetricMahler.symmetric_mahler, OAI.SymmetricMahler.symmetric_mahler_equality, OAI.SymmetricPolar.symmetric_polar_main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources