lean_workbook_plus_61523

Disproved

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

Hence \n\n

(x^2y+y^2z+z^2x)(xy^2+yz^2+zx^2)(xy+yz+zx)\ge \frac{(xy+yz+zx)^4}{3}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61523 : ∀ x y z : ℝ, (x^2*y + y^2*z + z^2*x) * (x*y^2 + y*z^2 + z*x^2) * (x*y + y*z + z*x) ≥ (x*y + y*z + z*x)^4 / 3   :=  by sorry

Source

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

View graph