VibeMathedMath problems solved with AI

The Mahler conjecture for general (non-symmetric) convex bodies

For a convex body K⊂RnK\subset\mathbb R^n and an interior point zz let (K−z)∘={y:⟨y,x−z⟩≤1 for all x∈K}(K-z)^\circ=\{y:\langle y,x-z\rangle\le1\ \text{for all}\ x\in K\}. The volume product P(K)=inf⁡z∈int K∣K∣ ∣(K−z)∘∣P(K)=\inf_{z\in\mathrm{int}\,K}|K|\,|(K-z)^\circ|, attained at the Santalo point, is invariant under invertible affine maps, and simplices give (n+1)n+1/(n!)2(n+1)^{n+1}/(n!)^2. Mahler proved the planar inequality among polygons; Meyer completed the planar equality case, Meyer and Reisner proved it for polytopes with at most n+3n+3 vertices, Kim and Reisner proved local minimality of simplices, and Chen, Li, Xi and Xu (2026) proved it in dimension three. Is P(K)≥(n+1)n+1/(n!)2P(K)\ge(n+1)^{n+1}/(n!)^2 for every convex body K⊂RnK\subset\mathbb R^n in every dimension, with equality only for simplices?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Convex geometry: volume products and polarity
Posed by
Kurt Mahler, as the manuscript frames the Mahler conjecture; planar case in Ein Minimalproblem fur konvexe Polygone, Mathematica (Zutphen) B7 (1938)
Year posed
—
Years open
—
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
55 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: for every n≥1n\ge1 and every convex body K⊂RnK\subset\mathbb R^n with Santalo point s(K)s(K), ∣K∣ ∣(K−s(K))∘∣≥(n+1)n+1/(n!)2|K|\,|(K-s(K))^\circ|\ge(n+1)^{n+1}/(n!)^2, with equality iff KK is a simplex; no symmetry or boundary regularity is assumed. The proof goes through Klartag's cone and Laplace-transform correspondence, Gaussian-averaged nearest-point projections onto a cone and its dual, and a spectral comparison whose scalar estimates rest on finite rational certificates with a released Python runner. Corollary: the sharp functional inequality ∫e−φ∫e−φ∗≥en\int e^{-\varphi}\int e^{-\varphi^*}\ge e^n for convex φ\varphi, via Fradelizi-Meyer, and an entropy-transport bound under an extra hypothesis. It does not give the symmetric constant 4n/n!4^n/n!, which is a separate entry.

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. OpenAI also released an abridged summary of the model's reasoning for this family (reasoning_traces/symmetric-and-general-mahler-conjectures.pdf).

Verification

No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 of the TeX source, read against the general Mahler problem as the manuscript states it; the proof was not refereed. Lean-checked on the release's own Comparator challenge GeneralMahler (OAI.GeneralMahler.general_mahler) together with its solution module OAI/Geometry/Convex/GeneralMahler/Theorem.lean, both present at the pinned commit. The challenge is not listed in the release's formalization catalogue (lean/formalization.yaml), though the family's scope note lean/docs/087.md links it. Its statement, read here, gives (n+1)n+1/(n!)2≤inf⁡z∈int K∣K∣ ∣(K−z)∘∣(n+1)^{n+1}/(n!)^2\le\inf_{z\in\mathrm{int}\,K}|K|\,|(K-z)^\circ| for every compact convex K⊆RnK\subseteq\mathbb R^n with nonempty interior, n≥1n\ge1, with equality iff KK is the convex hull of n+1n+1 affinely independent points: the headline claim in full. The functional inequality is not formalized. The statement was not independently audited and the development was not rebuilt here; the paper's ten verification programs were not re-run here.

Sources

Changelog1 change

Discussion