lean_workbook_plus_72687

Proved

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

For non-negative reals, we have $(a^3+b^3)^2=a^6+b^6+2a^3b^3\geqslant a^6+b^6$ and $(a+b)(a^5+b^5)=a^6+b^6+a^5b+ab^5\geqslant a^6+b^6$ ; with equality occuring in both cases if and only if $a=b=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72687 ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) : (a^3 + b^3)^2 ≥ a^6 + b^6 + 2 * a^3 * b^3   :=  by sorry

Source

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

View graph