lean_workbook_plus_6366

Proved

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

Prove that if $x,y>0$ then $\frac{x^3+y^3}{x^2+xy+y^2}-\frac{x+y}{3} = \frac{2(x+y)(x-y)^2}{3(x^2+xy+y^2)} \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6366 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (x^3 + y^3) / (x^2 + x * y + y^2) - (x + y) / 3 = 2 * (x + y) * (x - y)^2 / (3 * (x^2 + x * y + y^2)) ∧ 2 * (x + y) * (x - y)^2 / (3 * (x^2 + x * y + y^2)) >= 0   :=  by sorry

Source

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

View graph