lean_workbook_plus_20240

Proved

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

Prove that for all positive real $x$ , the following inequality holds: \n\n

(x + 1)(x + 2)(x + 5) \geq 36x.

\n\n Alternatively, we can note $f(x)=(x + 1)(x + 2)(x + 5) -36x$ , then we have: \n\n $f'(x)=(x-1)(3x+19)$ which means that for $x\geq 0$ , we have: \n\n $f(x) \geq f(1)=0$ Done.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20240  (x : ℝ)
  (h₀ : 0 < x) :
  (x + 1) * (x + 2) * (x + 5) ≥ 36 * x   :=  by sorry

Source

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

View graph