oai-math-revised beta

Browse › Convex and metric geometry › 087 The Mahler conjectures, functional inequalities and polar-product symplectic width

The symmetric Mahler conjecture and its equality cases

OpenAI · September 22, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We resolve the symmetric Mahler conjecture positively, including its equality classification. Every origin-symmetric convex body in ℝn has volume product at least $4^n/n!$, with equality exactly for invertible linear images of Hanner polytopes.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

Comments and discussion

Formalization

  • OpenAI math release, Lean scope note for family 087 (lean/docs/087.md). States that the formalization proves $|K||K^\circ|\ge4^n/n!$ for every $n\ge1$ with equality exactly for linear images of Hanner bodies, via the MahlerConjecture and SymmetricMahlerEquality comparators; the functional inequalities are excluded. [family-level]
  • OpenAI math release, MainTheorem.lean (symmetric_mahler) (openai/math, commit adc7f12). Lean statement of the symmetric inequality in every positive dimension; the equality classification is in a separate file and comparator challenge (SymmetricMahlerEquality.lean).
  • anxkhn, Add the symmetric Mahler volume-product inequality (google-deepmind/formal-conjectures issue #6972, 8 Oct 2026). Proposes adding Theorem 1.1 (inequality only, no equality cases or functional variants) to formal-conjectures; the author discloses AI assistance.
  • anxkhn, feat(Paper): add the symmetric Mahler inequality (google-deepmind/formal-conjectures PR #6977, opened 8 Oct 2026, open with one approving review on 10 Oct 2026). Adds the statement only; the PR says the external proof build was interrupted, so no formal_proof attribute is attached.

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

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

Lean formalization

OpenAI provides Lean files for this family: lean/docs/087.md. The Lean statements have not been checked by people against the paper's claims.

Family 087: The Mahler conjectures, functional inequalities and polar-product symplectic width

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.

Other papers in this family: