Prove2Me

lean_workbook_plus_65740

Disproved

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

4(yz(x3+t3)+xt(y3+z3))≤(x2+t2)2(y+z)+(y2+z2)2(x+t)4\left(yz(x^3+t^3)+xt(y^3+z^3)\right)\leq(x^2+t^2)^2(y+z)+(y^2+z^2)^2(x+t) .

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

View graph