lean_workbook_plus_9599

Proved

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

Put $a=\frac{1}{x},b=\frac{1}{y},c=\frac{1}{z}$ , then this inequality becomes \n $\frac{x^4+y^4+z^4}{x^4y^4z^4} \ge \frac{1}{xyz} ( \frac{1}{x^2y^3}+\frac{1}{y^2z^3}+\frac{1}{z^2x^3})$ \n $\Leftrightarrow x^4+y^4+z^4 \ge x^3y+y^3z+z^3x$ \nwhich is obviously true by AM-GM.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9599  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z) :
  x^4 + y^4 + z^4 ≥ x^3 * y + y^3 * z + z^3 * x   :=  by sorry

Source

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

View graph