Prove2Me

A symmetric product lower bound

Proved
WorkbookSource.problem_40872

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

lean-workbooksource-checked

For positive real x,y,zx,y,z,

(x2+yz)(y+z)≥4xyz.(x^2+yz)(y+z)\ge4xyz.

Source: InternLM Lean-Workbook, record lean_workbook_40872 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

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

View graph