lean_workbook_plus_72803

Proved

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

If $x,y>0$ , then prove: $x^4+y^4+x^2+y^2+2+2x(4x^2+1)+2y(4y^2+1)>18xy$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72803 (x y : ℝ) (hx : x > 0) (hy : y > 0) : x^4 + y^4 + x^2 + y^2 + 2 + 2 * x * (4 * x^2 + 1) + 2 * y * (4 * y^2 + 1) > 18 * x * y   :=  by sorry

Source

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

View graph