Vicente's question: is the Gromov width of every symmetric Lagrangian polar product equal to 4?

For an origin-symmetric convex body $K\subset\mathbb R^n$ put $K$ in position space and its polar $K^\circ$ in momentum space of $(\mathbb R^{2n},\sum_j dq_j\wedge dp_j)$ . Artstein-Avidan, Karasev and Ostrover (2014) proved that the Hofer-Zehnder capacity of $K\times K^\circ$ is 4 and showed that Viterbo's volume-capacity conjecture for these products implies the symmetric Mahler conjecture. The Gromov width $c_G$ is the supremum of $\pi r^2$ over symplectic embeddings of the radius- $r$ ball, so $c_G\le4$ ; equality was known for Euclidean balls, the cube (Ramos-Sepe) and $\ell_p$ balls (Karasev). Vicente noted that a positive answer immediately implies the Mahler conjecture. Is $c_G(K\times K^\circ)=4$ for every origin-symmetric convex body $K$ ?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Construction
Field: Symplectic geometry: capacities of Lagrangian products
Posed by: Alejandro Vicente, Questions related to the Mahler and the Viterbo Conjecture, blog post, 13 January 2026 (question 1)
Year posed: 2026
Years open: 0y
Solved: 2026-09-22
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 45 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: for every $n\ge2$ and every origin-symmetric convex body $K\subset\mathbb R^n$ , $c_G(\mathrm{int}\,K\times\mathrm{int}\,K^\circ)=4$ , with explicit smooth symplectic embeddings of every ball of capacity $c<4$ ; no smoothness or strict convexity is assumed. The lower bound comes from a holomorphic ball principle (high-order vanishing gives large balls) and a uniform slice estimate for a conformal lens; the upper bound from a supporting-cylinder argument and nonsqueezing. Since symplectic embeddings preserve volume this reproves the symmetric Mahler inequality, but the paper makes no claim about equality cases. It says nothing about non-symmetric products or other capacities, and does not conflict with the Haim-Kislev-Ostrover counterexample to Viterbo's general conjecture.

What the AI did

The OpenAI math release (github.com/openai/math, commit adc7f12) states that its results were produced by an unreleased internal OpenAI model under one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result, across roughly 4,000 posed problems; outputs were then grouped into families and filtered for significance. This result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is credited to OpenAI alone and names no human author. The README also cautions that unformalized results could have issues.

Verification

No independent mathematician has checked this yet. Checked here: the abstract, introduction, background section and Theorem 1.1 of the TeX source, and Vicente's blog post itself, whose first listed question is exactly this one; the proof was not refereed. Lean-checked on the Comparator challenge SymmetricPolar (OAI.SymmetricPolar.symmetric_polar_main, OAI/Geometry/PolarProducts/Main.lean), listed in the release's formalization catalogue. Its statement, read here, says that for $n\ge2$ and every compact convex symmetric $K$ with nonempty interior, the Gromov width of $\mathrm{int}\,K\times\mathrm{int}\,K^\circ$ (supremum over smooth embeddings preserving the standard form $\omega_0$ of open balls $\pi(|q|^2+|p|^2)<c$ ) equals 4, and that every ball with $0<c<4$ embeds: the headline claim. An embedding at capacity exactly 4 is not asserted. Permitted axioms: propext, Quot.sound, Classical.choice. The statement was not independently audited and the development was not rebuilt here.

Vicente's question: is the Gromov width of every symmetric Lagrangian polar product equal to 4?

What was actually shown

What the AI did

Verification

Sources

Discussion