lean_workbook_plus_15075

Disproved

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

prove that: \n $(a^2+b+\frac{3}{4})(b^2+a+\frac{3}{4})\geq (2a+\frac{1}{2})(2b+\frac{1}{2})$ \nfrom moroccan TST 2007

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15075 : ∀ a b : ℝ, (a^2 + b + 3 / 4) * (b^2 + a + 3 / 4) ≥ (2 * a + 1 / 2) * (2 * b + 1 / 2)   :=  by sorry

Source