lean_workbook_plus_68356

Disproved

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

for AM-GM \n\n $y(x+1)^2+x(y+1)^2 \ge 2\sqrt{xy}(x+1)(y+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68356 : ∀ x y : ℝ, y * (x + 1) ^ 2 + x * (y + 1) ^ 2 ≥ 2 * Real.sqrt (x * y) * (x + 1) * (y + 1)   :=  by sorry

Source