lean_workbook_plus_71704

Proved

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

Show $(a(a+1)+b(b+1))^{2}\ge \frac{8}{3}(ab(ab+1)+(a+b)(a^{2}+b^{2}))$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71704 (a b : ℝ) : (a * (a + 1) + b * (b + 1))^2 ≥ (8:ℝ) / 3 * (a * b * (a * b + 1) + (a + b) * (a^2 + b^2))   :=  by sorry

Source