OpenAI proves the Mahler conjectures (Lean)

Your AI and this story

Key facts

• Manuscripts (OpenAI, all dated 22 Sep 2026): ‘The symmetric Mahler conjecture and its equality cases’ (26 pp.), ‘The Mahler Conjecture for General Convex Bodies’ (72 pp.) and ‘Symplectic Balls in Symmetric Polar Products’ (19 pp.); a reasoning summary for this family is in the repository’s reasoning_traces folder
• Symmetric case (abstract, verbatim): ‘Every origin-symmetric convex body in ℝⁿ has volume product at least 4ⁿ/n!, with equality exactly for invertible linear images of Hanner polytopes.’ General case (abstract, verbatim): ‘For every convex body K ⊂ ℝⁿ, n ≥ 1, with Santaló point s(K), |K| |(K−s(K))°| ≥ (n+1)^{n+1}/(n!)², with equality exactly for simplices.’
• Symplectic companion (abstract, verbatim): ‘we prove that the Gromov width of int K × int K° is 4 … Volume preservation then resolves the symmetric Mahler conjecture positively in every dimension.’ (Artstein-Avidan, Karasev and Ostrover had shown in 2014 that Viterbo’s conjecture on symplectic capacities would imply the symmetric case)
• Prior state (symmetric paper, §1): Mahler proved the planar case; ‘Iriyeh and Shibata proved the complete three-dimensional symmetric theorem, including equality’, with a shorter proof by Fradelizi, Hubard, Meyer, Roldán-Pensado and Zvavitch; Saint-Raymond (unconditional bodies) and Reisner (zonoids) settled special classes; Bourgain and Milman proved the inequality up to a constant to the power n
• Lean: comparator challenges MahlerConjecture.lean (symmetric_mahler: for compact convex symmetric K ⊂ ℝⁿ with nonempty interior, 4ⁿ/n! ≤ vol(K)·vol(polar K), polar taken with the standard dot product), SymmetricMahlerEquality.lean, GeneralMahler.lean (general_mahler: the infimum over interior centres z of vol(K)·vol((K − z)°) is at least (n+1)ⁿ⁺¹/(n!)², with equality iff K is a simplex) and SymmetricPolar.lean. Scope note: ‘The nonsymmetric Mahler conjecture and the functional inequalities are not included’ in the symmetric file; the general file covers the nonsymmetric case. All four were accepted in the oai-math-revised comparator run (25–26 Oct). Our reading: the statements are the standard conjectures
• Reactions: Gil Kalai (7 Oct) put it first among twenty connections to his blog: ‘The release announces proofs of both the symmetric and general Mahler conjectures in every dimension, including the equality cases of Hanner polytopes and simplices, respectively.’ Martin Winter (arXiv 2610.09990, 7 Oct) proves a flag-number inequality and notes ‘This shows that the Mahler conjecture implies Kalai’s flag conjecture’
• Human digestion so far: Rotem Assouline’s web notes (updated 23 Oct) rewrite the symmetric proof and its equality case with figures; per the community notes they were written in conversation with Claude and the proof ‘has not been completely verified by the author’. Elliot Kienzle published an illustrated exposition of the symplectic-ball construction