lean_workbook_plus_49207

Proved

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

Let $x,y$ be positive numbers satisfying $x + y \le 1.$ Prove that $x^4 + y^4 - x^2y - xy^2\geq -\frac{1}{8}$ . Equality holds when $x=y=\frac{1}{2}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49207 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (hxy : x + y ≤ 1) : x^4 + y^4 - x^2*y - x*y^2 ≥ -1/8   :=  by sorry

Source

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

View graph