Prove2Me

lean_workbook_plus_3184

Proved

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

Using the AM-GM Inequality, we have 2y(1+x2+y2+z2)(x3+z3+xyz+xz)≤ ≤[y(1+x2+y2+z2)+2(x3+z3+xyz+xz)]24. \begin{aligned} 2y(1 + x^2 & + y^2 + z^2)(x^3 + z^3 + xyz + xz) \le \ & \le \frac {[y(1 + x^2 + y^2 + z^2) + 2(x^3 + z^3 + xyz + xz)]^2}{4}.\end{aligned}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3184 {x y z : ℝ} : 2*y*(1 + x^2 + y^2 + z^2)*(x^3 + z^3 + x*y*z + x*z) ≤ (y*(1 + x^2 + y^2 + z^2) + 2*(x^3 + z^3 + x*y*z + x*z))^2 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph