Prove2Me

lean_workbook_plus_5754

Proved

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

Prove that 36+2⋅p33≥18p  ⟺  (p−3)2(p+6)≥036+2\cdot\frac{p^3}{3} \ge 18p \iff (p-3)^2(p+6) \ge0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5754 (p : ℝ) : 36 + 2 * (p ^ 3 / 3) ≥ 18 * p ↔ (p - 3) ^ 2 * (p + 6) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph