lean_workbook_plus_1427

Proved

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

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph