The logarithmic Brunn–Minkowski conjecture

The logarithmic Brunn–Minkowski conjecture of Böröczky, Lutwak, Yang and Zhang asserts that, for origin-symmetric convex bodies, the logarithmic interpolation of support functions preserves the geometric-mean lower bound for volume. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claims a proof in every dimension, and the collection includes a Lean formalization of the volume inequality. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • The conjecture is Problem 1.1 of Böröczky, Lutwak, Yang and Zhang (2012), within the L_p Brunn–Minkowski theory of Firey and Lutwak; the logarithmic case is the endpoint p → 0 and is tied to cone-volume measures and the logarithmic Minkowski problem.
  • Earlier global results covered the plane (Böröczky, Lutwak, Yang and Zhang), bodies unconditional in a common basis (Saroglou), bodies invariant under the same n reflections (Böröczky and Kalantzopoulos), unit balls of complex norms (Rotem) and pairs sharing n − 2 orthogonal reflection symmetries (Lu). Stancu announced the all-dimensional logarithmic Minkowski inequality, with details of the flow asymptotics deferred.
  • Local versions were studied by Colesanti, Livshyts and Marsiglietti, by Kolesnikov and Milman (for p ≥ 1 − c·n^−3/2), by Chen, Huang, Li and Liu, by Putterman (equivalence of local and global inequalities), by van Handel (origin-symmetric zonoids) and by Milman.
  • Saroglou proved that the inequality for Lebesgue volume in dimension n implies the same inequality for every even log-concave measure in that dimension, and hence the (B)-conjecture for scalar dilations.

The original result

• Claim. Theorem 1.1 of The logarithmic Brunn–Minkowski conjecture states that for every n ≥ 1, all origin-symmetric convex bodies K, L ⊂ Rⁿ and 0 ≤ λ ≤ 1, the Wulff body of h_K^1−λh_L^λ has volume at least |K|^1−λ|L|^λ.
• Consequences stated in the manuscript. Corollary 1.2 gives the symmetric L_p Brunn–Minkowski inequality for 0 < p < 1. Through Saroglou's transfer and a support-subspace reduction, the manuscript also states the logarithmic inequality for every even log-concave Radon measure and the scalar-dilation (B)-conjecture.
• Method, as described: the slab constraints of a symmetric polytope are replaced by a smooth Gaussian-type weight, so that it suffices to prove log-concavity of its integral under geometric changes of the slab widths. This reduces to a variance bound for sums of even powers of linear forms, which is proved in moment coordinates (building on Berman–Berndtsson and Klartag) through a density argument for centered even test functions and a tensor calculation whose remainder is a sum of explicit squares.
• Source. The manuscript The logarithmic Brunn–Minkowski conjecture at commit 1581d4c.
• Formalization. The repository's scope note states that the formalized result proves, for every dimension n ≥ 1, origin-symmetric convex bodies K, L and 0 ≤ t ≤ 1, that their logarithmic Wulff combination has volume at least |K|^1−t|L|^t, assuming neither boundary smoothness nor unconditionality. Its Comparator statement is LogBrunnMinkowski.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 19 October 2026)
2026-10-07	Y. Liu, Q. Sun, G. Xiong, The centered logarithmic Brunn–Minkowski inequality (arXiv:2610.10152, v2 of 8 October 2026)	Extension	The abstract states the logarithmic Brunn–Minkowski and logarithmic Minkowski inequalities for convex bodies whose centroids are at the origin, with equality precisely for independent positive dilations of common direct summands, and the Lp Brunn–Minkowski and Minkowski inequalities for every p > 0, with uniqueness of centered Lp surface area measures. The paper states that its analytic starting point is the moment-coordinate argument of the manuscript, whose adjoint identities and tensor calculation it reproduces without symmetry assumptions. Its authors' note states that the work was developed with GPT after the manuscript's release, that separate GPT sessions were used for adversarial checks, and that the authors had not yet completed an independent verification, so the work is presented as a proposed proof requiring further scrutiny.	arXiv preprint.
2026-10-08	MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "partial" and records a sandboxed Comparator pass for the challenge LogBrunnMinkowski. Its note states that only the Lebesgue-volume inequality is stated in Lean, and that the (B)-conjecture for even log-concave measures and the Lp inequality for 0 < p < 1 are not.	The review states that it does not say the mathematics is correct beyond what Lean checked; it describes itself as a model-assisted reading without a referee yet.
2026-10-08	Formal Conjectures pull request #6978	Statement (proposed)	Proposes adding the origin-symmetric logarithmic Brunn–Minkowski inequality in every positive dimension to the repository, citing the manuscript's main theorem at commit adc7f12. The description reports that a bridge applies the collection's Lean theorem to the proposed statement with only the standard axioms. Measure extensions, equality cases and the Lp consequences are outside the pull request.	Open pull request (not merged when checked).
2026-10-11	vortex-QC/logbm-pilot (GitHub, commit 0a29f77)	Partial replication (Lean)	The README describes a pilot independent replication, in Lean 4 with Mathlib, of two minimal slices of the collection's formalization: the one-dimensional volume identity by a different route, and the smallest instance of the soft-variance statement (dimension two, one direction, q = 2). It reports zero sorry and only the standard axioms for the main theorems, and states that it is not a re-formalization of the full proof.	GitHub repository; the README states that a Zenodo record is pending.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.