Prove2Me

lean_workbook_plus_36600

Disproved

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

if 0≤x≤10\leq x \leq1 then g(x)=−2x2+2x+2=−2(x−1/2)2+54≤54g(x)=-2x^2+2x+2=-2(x-1/2)^2+\frac{5}4\leq\frac{5}4

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36600 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) :
  -2 * x ^ 2 + 2 * x + 2 ≤ 5 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph