lean_workbook_plus_53259

Proved

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

For $a,b\ge 0$ such that $a^2\ge 4b$ . Prove that: $5(a^2b^2-ab)+8\ge 9b^2(b+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53259 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a^2 ≥ 4 * b) : 5 * (a^2 * b^2 - a * b) + 8 ≥ 9 * b^2 * (b + 1)   :=  by sorry

Source

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

View graph