Prove2Me

lean_workbook_plus_15814

Disproved

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

And when f(x)=−x3+ax2+bx+c=−(x−2)3+34(x−2),f(x)=-x^3+ax^2+bx+c=-(x-2)^3+\frac{3}{4}(x-2), where a=6,b=−454,c=132,a=6,b=-\frac{45}{4},c=\frac{13}{2}, we have M=14.M=\frac{1}{4}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15814  (a b c : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = -x^3 + a * x^2 + b * x + c)
  (h₁ : a = 6)
  (h₂ : b = -45 / 4)
  (h₃ : c = 13 / 2)
  (h₄ : ∀ x, f x = -(x - 2)^3 + (3 / 4) * (x - 2)) :
  ∃ x, (f x = 0 ∧ 0 < x ∧ x < 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph