AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

The symmetric Mahler conjecture and its equality cases

Can the mathematical statement in The symmetric Mahler conjecture and its equality cases be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 087)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The symmetric Mahler conjecture and its equality cases'. We resolve the symmetric Mahler conjecture positively, including its equality classification. Every origin-symmetric convex body in ℝn has volume product at least 4^n/n!, with equality exactly for invertible linear images of Hanner polytopes.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 087). The Lean development was not rebuilt locally.