Prove2Me

An eighth-power bound for pairwise symmetric products

Proved
WorkbookSource.plus_73339

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

lean-workbooksource-checked

Let x≥0,x\geq0, y≥0,y\geq0, z≥0.z\geq0. Prove that (x+y+z)8≥243(xy+xz+yz)2(x2y2+x2z2+y2z2).(x+y+z)^{8}\geq243(xy+xz+yz)^{2}(x^{2}y^{2}+x^{2}z^{2}+y^{2}z^{2}).

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_73339 (x y z : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : (x + y + z) ^ 8 ≥ 243 * (x * y + x * z + y * z) ^ 2 * (x ^ 2 * y ^ 2 + x ^ 2 * z ^ 2 + y ^ 2 * z ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_73339; Apache-2.0

View graph