OpenAI claim summary for Math-2647
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 087; 2026-09-22).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Gromov width of symmetric polar products
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.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.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.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 central assertion is within the documented formal scope; the additional applications retain their own scope limits.
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
- OpenAI, Symplectic Balls in Symmetric Polar Products, 2026-09-22; citation key
OAI:Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 087: Lean scope.
- Comparator GeneralMahler.json.
- Comparator GeneralMahler.lean.
- Comparator MahlerConjecture.json.
- Comparator MahlerConjecture.lean.
- Comparator SymmetricMahlerEquality.json.
- Comparator SymmetricMahlerEquality.lean.
- Comparator SymmetricPolar.json.
- Comparator SymmetricPolar.lean.
- Family 087: Reasoning summary.
- OpenAI catalogue entry.