lean_workbook_plus_4424

Proved

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

Prove that $x^2+\frac{8}{xy}+y^2\ge 8$ for all positive real numbers x and y.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4424 (x y : ℝ) (h₀ : 0 < x) (h₁ : 0 < y) : x^2 + (8/(x*y)) + y^2 >= 8   :=  by sorry

Source