Prove2Me

lean_workbook_plus_64968

Disproved

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

⇔3(x−1)2(−3x10+34x9−157x8+444x7−1061x6+1970x5−1803x4+256x3+216x2+144x+216)8x4(3−x)4≥0\Leftrightarrow \frac{3 (x - 1)^2 (-3 x^{10} + 34 x^9 - 157 x^8 + 444 x^7 - 1061 x^6 + 1970 x^5 - 1803 x^4 + 256 x^3 + 216 x^2 + 144 x +216)}{8x^4(3-x)^4} \ge 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64968 : ∀ x : ℝ, (3 * (x - 1) ^ 2 * (-3 * x ^ 10 + 34 * x ^ 9 - 157 * x ^ 8 + 444 * x ^ 7 - 1061 * x ^ 6 + 1970 * x ^ 5 - 1803 * x ^ 4 + 256 * x ^ 3 + 216 * x ^ 2 + 144 * x + 216)) / (8 * x ^ 4 * (3 - x) ^ 4) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph