A twelfth-degree pair-sum product inequality

Proved

WorkbookSource.base_19323

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that for positive real numbers $x$ , $y$ , and $z$ , the inequality $3^3 \left( {x + y} \right)^4 \left( {y + z} \right)^4 \left( {z + x} \right)^4 \ge 2^{12} x^3 y^3 z^3 \left( {x + y + z} \right)^3$ holds.

Source: InternLM Lean-Workbook, record lean_workbook_19323 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_19323    (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
  3^3 * (x + y)^4 * (y + z)^4 * (z + x)^4 ≥ 2^12 * x^3 * y^3 * z^3 * (x + y + z)^3  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_19323; Apache-2.0

View graph