---
id: "2026-10-06-openai-mahler-conjecture-lean"
url: "https://postcutoff.com/e/2026-10-06-openai-mahler-conjecture-lean/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 11
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-mahler-conjecture-lean/

# OpenAI proves the Mahler conjectures (Lean)

Full title: OpenAI's release proves both Mahler volume-product conjectures (1939) in every dimension, with equality cases, and formalizes them in Lean

Three manuscripts dated 22 Sep 2026 (family 087 of OpenAI's 6 Oct release) claim the Mahler conjecture in every dimension: every origin-symmetric convex body K ⊂ ℝⁿ has |K||K°| ≥ 4ⁿ/n!, with equality exactly for linear images of Hanner polytopes, and every convex body has |K||(K − s(K))°| ≥ (n+1)ⁿ⁺¹/(n!)², with equality exactly for simplices. A third paper shows that the Gromov width of K × K° is 4, which by volume comparison gives the symmetric case again. Before, the symmetric case was proved in dimensions 2 and 3, and the best general bound, Bourgain–Milman, was off by an exponential factor. OpenAI's Lean formalization covers the symmetric and general inequalities with their equality cases; the functional versions are not formalized. The papers are unrefereed.

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

## What happened

For a convex body K and its polar K°, the product of their volumes does not change under linear maps. Blaschke and Santaló found the
maximum (the ball); Kurt Mahler asked in 1939 for the minimum. He conjectured that for symmetric bodies the cube and its polar, the
cross-polytope, are extremal, with volume product 4ⁿ/n!, and that for general bodies the simplex is. The symmetric case was proved in
the plane by Mahler and in three dimensions only in 2020 (Iriyeh–Shibata), and Bourgain and Milman's 1987 theorem gives the right
answer only up to a factor cⁿ.

OpenAI's release contains three manuscripts dated 22 Sep that claim both conjectures in every dimension, with the full equality
cases: Hanner polytopes (built from intervals by products and dual products) in the symmetric case and simplices in general. The
third paper takes a symplectic route: it embeds balls of every capacity below 4 into K × K°, so the Gromov width is 4 and the volume
bound follows. Lean comparator statements cover the symmetric and general inequalities with equality, defined from Mathlib's
Lebesgue measure and the ordinary dot-product polar; they read as the standard conjectures, and all four passed the community run.

## Why it matters

Mahler's conjecture is one of the best-known open problems in convex geometry, with links to the geometry of numbers, functional
analysis and symplectic capacities. Lean proofs of the exact statements make the claim unusually checkable; what remains is human
understanding of why the argument works.

## What is disputed or not yet verified

- Verification: Lean formalization of both inequalities and equality cases (comparator accepted); no published expert verification yet

## Reactions

Gil Kalai, who has written about the symmetric conjecture and its links to his flag conjecture, listed the claim first in his survey
of the release. Martin Winter observed the next day that the Mahler conjecture, combined with his new inequality, implies Kalai's
flag conjecture. Human expositions of the proof are in progress, but none so far claims a complete check.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI: The symmetric Mahler conjecture and its equality cases (22 Sep)](https://github.com/openai/math/blob/main/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf) (github.com, paper)
2. [OpenAI: The Mahler Conjecture for General Convex Bodies (22 Sep)](https://github.com/openai/math/blob/main/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/paper.pdf) (github.com, paper)
3. [OpenAI: Symplectic Balls in Symmetric Polar Products (22 Sep)](https://github.com/openai/math/blob/main/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026/paper.pdf) (github.com, paper)
4. [Lean scope note for family 087](https://github.com/openai/math/blob/main/lean/docs/087.md) (github.com, code)
5. [Lean comparator challenge: GeneralMahler.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/GeneralMahler.lean) (github.com, code)
6. [Lean comparator challenge: MahlerConjecture.lean (symmetric case)](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/MahlerConjecture.lean) (github.com, code)
7. [arXiv 2610.09990: Martin Winter, A relation between Mahler volume and flag number for convex polytopes](https://arxiv.org/abs/2610.09990) (arxiv.org, paper)
8. [oai-math-revised: comparator run on all challenges (LEAN_CHECKS.md)](https://github.com/mathcommunity/oai-math-revised/blob/main/docs/LEAN_CHECKS.md) (github.com, code)
9. [Gil Kalai: Updates: Sharing AI progress on mathematics (amazing!) (7 Oct)](https://gilkalai.wordpress.com/2026/10/07/updates-sharing-ai-progress-on-mathematics-amazing-and-my-lecture-plans/) (gilkalai.wordpress.com, discussion)
10. [Rotem Assouline: Notes on OpenAI's proof of the symmetric Mahler conjecture](https://rotemassouline.github.io/symmetric-mahler/) (rotemassouline.github.io, discussion)
11. [oai-math-revised: notes on the symmetric Mahler manuscript](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/NOTES.md) (github.com, discussion)

## Changes

- 2026-10-29 (filed): Created (families 001–125; manuscript abstracts and introductions, Lean statements, comparator results, Kalai's post and Winter's arXiv abstract read)

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)