Prove2Me

lean_workbook_plus_77380

Disproved

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

Prove the inequality 9∑cycx2(x2+y2)(x2+z2)+18∑cycxy(x2+y2)(x2+z2)(y2+z2)≥4(x+y+z)2(x2+y2+z2)29\sum_{cyc}x^2(x^2+y^2)(x^2+z^2)+18\sum_{cyc}xy(x^2+y^2)\sqrt{(x^2+z^2)(y^2+z^2)}\geq 4(x+y+z)^2(x^2+y^2+z^2)^2

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

View graph