Prove2Me

lean_workbook_plus_3613

Disproved

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

By Cauchy-Schwarz\n(x+y+z)(xy3+yz3+zx3)=(∑(z)2)(∑(xy3)2)≥(∑xy3z)2=xyz(x+y+z)2(x+y+z)(xy^3+yz^3+zx^3) =\left(\sum (\sqrt{z})^2\right)\left(\sum (\sqrt{xy^3})^2\right) \ge \left(\sum \sqrt{xy^3z}\right)^2 = xyz(x+y+z)^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3613 : ∀ x y z : ℝ, (x + y + z) * (x * y ^ 3 + y * z ^ 3 + z * x ^ 3) ≥ x * y * z * (x + y + z) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph