lean_workbook_plus_65634

Proved

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

For $a, b, c \geq 0$ , prove that $2+2(a^4+b^4)\geq ab^3+ba^3+a^3+b^3+a+b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65634 (a b c : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) : 2 + 2 * (a ^ 4 + b ^ 4) ≥ a * b ^ 3 + b * a ^ 3 + a ^ 3 + b ^ 3 + a + b   :=  by sorry

Source

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

View graph