lean_workbook_plus_81985

Proved

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

Let $a=x/2y,b=y/2z,c=z/2x$ and you get: $4x^4z^2+4y^4x^2+4z^4y^2+x^4y^2+z^4x^2+y^4z^2 \ge 15x^2y^2z^2$ which is true by AM-GM.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81985  (x y z : ℝ) :
  4 * x^4 * z^2 + 4 * y^4 * x^2 + 4 * z^4 * y^2 + x^4 * y^2 + z^4 * x^2 + y^4 * z^2 ≥ 15 * x^2 * y^2 * z^2   :=  by sorry

Source

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

View graph