lean_workbook_plus_68079

Proved

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

2> If $x+y>0$ then square all of them we have to solve the new inequality: $V(x,y)=8(x^2-xy+y^2)^2-(x^2+y^2)(x^2+2xy+y^2)\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68079 (x y : ℝ) (h : x + y > 0) : 8 * (x ^ 2 - x * y + y ^ 2) ^ 2 - (x ^ 2 + y ^ 2) * (x ^ 2 + 2 * x * y + y ^ 2) ≥ 0   :=  by sorry

Source

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

View graph