Prove2Me

A product of quadratic differences bounds the sixth power of the total

Proved
WorkbookSource.base_53586

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

lean-workbooksource-checked

Prove with x,y,z>0x,y,z>0 that (7x2+(y+z)2−x(y+z))(7y2+(x+z)2−y(x+z))(7z2+(x+y)2−z(x+y))≧(x+y+z)6(7x^2+(y+z)^2-x(y+z))(7y^2+(x+z)^2-y(x+z))(7z^2+(x+y)^2-z(x+y)) \geqq(x+y+z)^6

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

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

View graph