Prove2Me

lean_workbook_plus_19001

Proved

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

The Alternative :\n\n (a2−ab+b2)(a+b)4≥16a3b3(a^2-ab+b^2)(a+b)^4\geq 16a^3b^3 \n\n ⟺(1−x+x2)(1+x)4≥16x3\Longleftrightarrow (1-x+x^2)(1+x)^4\geq 16x^3 with x=ba>0x=\frac{b}{a}>0 \n\n ⟺(1+x3)(1+x)3x3≥16 (x>0).\Longleftrightarrow \frac{(1+x^3)(1+x)^3}{x^3}\geq 16\ (x>0).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19001 (x : ℝ) (hx : 0 < x) : ((1 + x^3) * (1 + x)^3) / x^3 ≥ 16   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph