Prove2Me

lean_workbook_plus_61910

Proved

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

Proof :\n\nLet f(x)=(1+x3)(1+x)3x3 (x>0)⟹f′(x)=3(x+1)3x6(x−1)f(x)=\frac{(1+x^3)(1+x)^3}{x^3}\ (x>0)\Longrightarrow f'(x)=\frac{3(x+1)^3}{x^6}(x-1) , yielding\n\n f(x)≥f(1)f(x)\geq f(1) , or f(x)≥16. Q.E.D.f(x)\geq 16.\ Q.E.D.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61910 (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