# Logarithmic and <i>L</i><sub><i>p</i></sub> Brunn–Minkowski inequalities and the B-conjecture

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

- [The logarithmic Brunn–Minkowski conjecture](../../preprints/The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/LogBrunnMinkowski.lean) |