Prove LogBrunnMinkowski (openai/math family 091: The logarithmic Brunn–Minkowski conjecture) in Lean 4 with…
Prove LogBrunnMinkowski (openai/math family 091: The logarithmic Brunn–Minkowski conjecture) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 091 of the release, The logarithmic Brunn–Minkowski conjecture (Convex and metric…
The task
Context: this statement belongs to family 091 of the release, *The logarithmic Brunn–Minkowski conjecture* (Convex and metric geometry). The family as a whole: Proves the logarithmic Brunn–Minkowski inequality for origin-symmetric convex bodies in every dimension, and the scalar-dilation B-conjecture for all even…
Part of raising-heart/openai-math.