lean_workbook_plus_8985

Proved

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

Let $a$ , $b$ be two non-negative real numbers such that $ab+a+b=3$ . Prove that $4\le ab(a^2+b^2)+a^3+b^3\le 27$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8985 (a b : ℝ) (hab : 0 ≤ a ∧ 0 ≤ b) (habp : a * b + a + b = 3) : 4 ≤ a * b * (a ^ 2 + b ^ 2) + a ^ 3 + b ^ 3 ∧ a * b * (a ^ 2 + b ^ 2) + a ^ 3 + b ^ 3 ≤ 27   :=  by sorry

Source

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

View graph