Logarithmic and L_p Brunn–Minkowski inequalities and the B-conjecture

1 paperLean

Proves the logarithmic Brunn–Minkowski inequality for origin-symmetric convex bodies in every dimension, and the scalar-dilation B-conjecture for all even log-concave Radon measures. For Lebesgue volume it also proves the additive L_p Brunn–Minkowski inequality for full-dimensional origin-symmetric convex bodies throughout \(0\lt p\lt 1\).

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The logarithmic Brunn–Minkowski conjecture

OpenAI · September 23, 2026

We prove the logarithmic Brunn–Minkowski conjecture for arbitrary origin-symmetric convex bodies in every dimension. The theorem also gives the symmetric L_p 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.

Read PDF Download Source

Cite

@misc{OAI:The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{The logarithmic Brunn--Minkowski conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026/paper.pdf}{OAI:The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The logarithmic Brunn–Minkowski conjecture

Scope

The logarithmic Brunn–Minkowski conjecture asserts that logarithmic interpolation of origin-symmetric convex bodies preserves the geometric-mean lower bound for volume. The formalized result proves, for every dimension \(n\ge1\), such bodies \(K,L\subset\mathbb R^n\), and \(0\le t\le1\), that their logarithmic Wulff combination has volume at least \(|K|^{1-t}|L|^t\). It assumes neither boundary smoothness nor coordinatewise unconditionality.

Comparator links

Result	Comparator statement
Logarithmic Brunn–Minkowski inequality	LogBrunnMinkowski.lean

Scope note on GitHub →