lean_workbook_plus_29928

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

In triangle, prove that $\left( y-z \right) ^{2} \left( 13\,{x}^{3}+34\,{x}^{2}y+36\,{x}^{2}z+y{z}^{2} \right) + \left( x-z \right) ^{2} \left( {x}^{2}y+3\,{x}^{2}z+5\,{y}^{2}z+9\,x{z}^{2} \right) + \left( x-y \right) ^{4}z+ \left( x-y \right) ^{2} \left( 9\,x{y}^{2}+3\,{x}^{2}y \right) +2\, \left( xy-2\,xz+yz \right) ^{2}y\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29928 {x y z : ℝ} (hx : x > 0 ∧ y > 0 ∧ z > 0) (hxy : x + y > z) (hxz : x + z > y) (hyz : y + z > x) :  (y - z) ^ 2 * (13 * x ^ 3 + 34 * x ^ 2 * y + 36 * x ^ 2 * z + y * z ^ 2) + (x - z) ^ 2 * (x ^ 2 * y + 3 * x ^ 2 * z + 5 * y ^ 2 * z + 9 * x * z ^ 2) + (x - y) ^ 4 * z + (x - y) ^ 2 * (9 * x * y ^ 2 + 3 * x ^ 2 * y) + 2 * (x * y - 2 * x * z + y * z) ^ 2 * y ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph