Prove2Me

lean_workbook_plus_61957

Proved

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

Show that (x−1)(x−2)(x−4)(x−5)≥−94(x-1)(x-2)(x-4)(x-5) \geq \frac{-9}{4} for all xx .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61957 : ∀ x, (x - 1) * (x - 2) * (x - 4) * (x - 5) ≥ (-9 / 4)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph