A cubic correction at sum three quarters

Proved

WorkbookSource.plus_30530

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

The $a,b\ge 0$ such that $a+b=\frac{3}{4}$ . Prove that $a^2-a^3+b^2-b^3\le \frac{45}{256}$ .

Source: InternLM Lean-Workbook, record lean_workbook_plus_30530 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_30530 (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 3 / 4) : a^2 - a^3 + b^2 - b^3 ≤ 45 / 256   :=  by sorry

Source