Prove2Me

lean_workbook_plus_11021

Proved

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

⇒4q⩾4(36p+72−p363−4p)⩾p+9⇔(p−3)(4p2+8p−93)⩽0, true for all 3⩽p<319.\Rightarrow 4q \geqslant 4 \left(\frac{36p+72-p^3}{63-4p} \right) \geqslant p+9 \Leftrightarrow \left(p-3 \right) \left(4p^2 + 8p - 93 \right) \leqslant 0, \ \text{true for all} \ 3 \leqslant p < \frac{31}{9}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11021 (p : ℝ) (hp : 3 ≤ p ∧ p < 31 / 9) (q : ℝ) (hq : q = (36 * p + 72 - p ^ 3) / (63 - 4 * p)) : p + 9 ≤ 4 * q   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph