Oct 6, 2026
Lean formalization in OpenAI math repository (Result 087)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Symplectic Balls in Symmetric Polar Products'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 087). The Lean development was not rebuilt locally.