Prove2Me

lean_workbook_plus_65968

Proved

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

5(x2+y2)2≤4+(x+y)4  ⟺  x4+y4+x2y2≤1+x3y+xy35 (x^2+ y^2) ^2 \leq 4 + (x +y) ^4\iff x^4+ y^4+x^2y^2\le 1+x^3y+ xy^3
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65968 (x y : ℝ) : 5 * (x ^ 2 + y ^ 2) ^ 2 ≤ 4 + (x + y) ^ 4 ↔ x ^ 4 + y ^ 4 + x ^ 2 * y ^ 2 ≤ 1 + x ^ 3 * y + x * y ^ 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph