Prove2Me

lean_workbook_plus_12234

Proved

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

(x2+y2+(x+y)2)((x−y)4+(2x+y)4+(2y+x)4)≥((x+y)22+(x+y)2)×2(2x+y)2(2y+x)2(x^{2}+y^{2}+(x+y)^{2})\left( (x-y)^{4}+(2x+y)^{4}+(2y+x)^{4}\right) \geq \left( \frac{\left( x+y\right) ^{2}}{2}+(x+y)^{2}\right) \times2(2x+y)^{2}(2y+x)^{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12234 (x y : ℝ) : (x^2 + y^2 + (x + y)^2) * ((x - y)^4 + (2 * x + y)^4 + (2 * y + x)^4) ≥ ((x + y)^2 / 2 + (x + y)^2) * (2 * (2 * x + y)^2 * (2 * y + x)^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph