lean_workbook_plus_75055

Proved

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

Let $x , y>0$ and $3(x+y) \geq 2(xy+1)$ . Prove that $x^2+y^2 \geq \frac{2}{7}(x^2y^2+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75055 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (h : 3 * (x + y) ≥ 2 * (x * y + 1)) : x ^ 2 + y ^ 2 ≥ 2 / 7 * (x ^ 2 * y ^ 2 + 1)   :=  by sorry

Source

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

View graph