lean_workbook_plus_24992

Proved

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

Prove that for all reals $x,y,$ $9x^2y^2+4x^2+54xy^2+24x+81y^2+36 \geq 12x^2y + 72xy+108y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24992 (x y : ℝ) : 9 * x ^ 2 * y ^ 2 + 4 * x ^ 2 + 54 * x * y ^ 2 + 24 * x + 81 * y ^ 2 + 36 ≥ 12 * x ^ 2 * y + 72 * x * y + 108 * y   :=  by sorry

Source

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

View graph