AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

The logarithmic Brunn–Minkowski conjecture

Can the mathematical statement in The logarithmic Brunn–Minkowski conjecture 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 091)

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 logarithmic Brunn–Minkowski conjecture'. We prove the logarithmic Brunn–Minkowski conjecture for arbitrary origin-symmetric convex bodies in every dimension. The theorem also gives the symmetric Lp Brunn–Minkowski inequality for every 0\lt p\lt 1. Combined with Saroglou's transfer theorem and a support-subspace reduction, it yields the logarithmic inequality for every even log-concave Radon measure and the scalar-dilation (B)-conjecture.

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