lean_workbook_plus_35983

Disproved

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

Replace $(a,b,c) \to (x+y,y+z,z+x)$ your inequality become\n $5(x^3+y^3+z^3) +19(x^2y+y^2z+z^2x) \geqslant 30xyz + 14(xy^2+yz^2+zx^2),$ equivalent to\n $\sum\frac{(x^2+9y^2+50yz)(x-y)^2}{2(x+y+z)} \geqslant 0.$ Done.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35983 :
  ∀ x y z : ℝ,
    5 * (x^3 + y^3 + z^3) + 19 * (x^2 * y + y^2 * z + z^2 * x) ≥ 30 * x * y * z + 14 * (x * y^2 + y * z^2 + z * x^2)   :=  by sorry

Source

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

View graph