lean_workbook_plus_44319

Proved

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

Prove the inequality for $x>0, y>0$ : \nx^4+y^4+(x^2+1)(y^2+1) >= (|y|+1)|x|^3+(|x|+1)|y|^3+|x|+|y|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44319 (x y : ℝ) (hx : x > 0) (hy : y > 0) : x^4 + y^4 + (x^2 + 1) * (y^2 + 1) ≥ (abs y + 1) * abs x^3 + (abs x + 1) * abs y^3 + abs x + abs y   :=  by sorry

Source

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

View graph