The Mahler conjectures
The Mahler conjectures are the subject of three manuscripts dated 22 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Claim. The symmetric and the nonsymmetric geometric Mahler conjectures hold in every dimension, with Hanner polytopes and simplices as the respective minimizers of the volume product and all equality cases classified; the corresponding sharp functional Mahler inequalities also hold. For n ≥ 2, every symmetric polar product K × K° in dimension 2n has Gromov width 4 (summary in the collection's contents list).
- Sources (openai/math repository, commit
adc7f12): - Formalization, as described by the repository. The scope note lean/docs/087.md states that the Lean formalization proves |K||K°| ≥ 4n/n! for every origin-symmetric convex body in every dimension, with equality exactly for invertible linear images of Hanner bodies; the general lower bound infz |K||(K − z)°| ≥ (n + 1)n+1/(n!)2 with equality exactly for simplices; and Gromov width 4 for int K × int K° when n ≥ 2 (an embedding at capacity exactly 4 is not asserted). The functional inequalities are outside the formalized statements. The comparator statements are listed in that note.
- Catalogue status. The AIM open-problem collection (MColbrook/AIM, not affiliated with the American Institute of Mathematics) records its problem 086 (the symmetric Mahler inequality in four dimensions) as solved by the symmetric manuscript, after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
- Earlier published results. H. Iriyeh and M. Shibata proved the symmetric conjecture in dimension 3, with its equality condition (arXiv:1706.01749). For background on the volume product, see the survey of M. Fradelizi, M. Meyer and A. Zvavitch (arXiv:2301.06131).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 13 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | K. Kitamura, funk-volume-kalai-flags (GitHub) | Use | A Lean 4 proof of Kalai's full flag conjecture: every centrally symmetric n-dimensional convex polytope has at least 2nn! complete flags. Also a Lean proof of the numerical symmetric Funk-volume lower bound. The README cites OpenAI's Lean module OAI.Analysis.Mahler (the flux, Stokes and holomorphic mass proofs) as used in the argument. |
Lean repository with statements in the style of Google DeepMind's formal-conjectures project and a Lean4Web link. The README states that the work was produced with assistance from ChatGPT and OpenAI Codex (GPT-6 Astra and GPT-6.1 Sol). |
| 2026-10-07 (manuscript date) | R. Gounder, Mathematical Frontiers in the OpenAI Research Release (GitHub) | Comparative review | Includes a case study of the Mahler manuscripts. A footnote observes that in the scope note a sentence excluding the nonsymmetric Mahler conjecture conflicts with the linked general-Mahler comparator target, which states the general inequality with simplex equality. | A 25-page review. The README states that its checks "do not independently establish the underlying release theorems". |
| 2026-10-13 | R. Assouline, Notes on OpenAI's proof of the symmetric Mahler conjecture (source) | Exposition | Notes rewriting the details of the symmetric proof (complexification, submanifolds of the polydisc, a lower bound on the volume of a holomorphic image, the equality case), with figures and interactive applets. | Work in progress, based on conversations with Claude. The author states: "I do not claim to have verified the proof completely." |
Notes
- The follow-ups state AI assistance as recorded in the table.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.