The Mahler conjectures: Difference between revisions
New result page: the Mahler conjectures, with public follow-ups (sources linked); Main Page link |
New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link |
||
| Line 8: | Line 8: | ||
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026 ''Symplectic Balls in Symmetric Polar Products'']. | ** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026 ''Symplectic Balls in Symmetric Polar Products'']. | ||
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/087.md lean/docs/087.md] states that the Lean formalization proves |''K''||''K''°| ≥ 4<sup>''n''</sup>/''n''! for every origin-symmetric convex body in every dimension, with equality exactly for invertible linear images of Hanner bodies; the general lower bound inf<sub>''z''</sub> |''K''||(''K'' − ''z'')°| ≥ (''n'' + 1)<sup>''n''+1</sup>/(''n''!)<sup>2</sup> 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. | * '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/087.md lean/docs/087.md] states that the Lean formalization proves |''K''||''K''°| ≥ 4<sup>''n''</sup>/''n''! for every origin-symmetric convex body in every dimension, with equality exactly for invertible linear images of Hanner bodies; the general lower bound inf<sub>''z''</sub> |''K''||(''K'' − ''z'')°| ≥ (''n'' + 1)<sup>''n''+1</sup>/(''n''!)<sup>2</sup> 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 ([https://github.com/MColbrook/AIM MColbrook/AIM], not affiliated with the American Institute of Mathematics) records its problem [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/086-mahler-symmetric-four-dimensions.md 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 ([https://arxiv.org/abs/1706.01749 arXiv:1706.01749]). For background on the volume product, see the survey of M. Fradelizi, M. Meyer and A. Zvavitch ([https://arxiv.org/abs/2301.06131 arXiv:2301.06131]). | * '''Earlier published results.''' H. Iriyeh and M. Shibata proved the symmetric conjecture in dimension 3, with its equality condition ([https://arxiv.org/abs/1706.01749 arXiv:1706.01749]). For background on the volume product, see the survey of M. Fradelizi, M. Meyer and A. Zvavitch ([https://arxiv.org/abs/2301.06131 arXiv:2301.06131]). | ||
Latest revision as of 11:17, 13 October 2026
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.