Prove2Me

lean_workbook_plus_44570

Disproved

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

Prove that 4(x+y)(y+z)(z+x)≥4zx(2y+z+x)+y(2z+x+y)(2x+y+z)4(x+y)(y+z)(z+x) \geq 4zx(2y+z+x)+y(2z+x+y)(2x+y+z)

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

View graph