lean_workbook_plus_68854

Disproved

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

$87u^3 + 21u^2 - 72u - 54 + 12u^5 + 60u^4 + 16\sqrt {3}u^2 + 32\sqrt {3}u + 32\sqrt {3}\geq (21 + 16\sqrt {3})u^2 - (72 - 32\sqrt {3})u + 32\sqrt {3} - 54$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68854 : ∀ u : ℝ, 12 * u ^ 5 + 60 * u ^ 4 + 87 * u ^ 3 + 21 * u ^ 2 - 72 * u - 54 + 16 * Real.sqrt 3 * u ^ 2 + 32 * Real.sqrt 3 * u + 32 * Real.sqrt 3 ≥ (21 + 16 * Real.sqrt 3) * u ^ 2 - (72 - 32 * Real.sqrt 3) * u + 32 * Real.sqrt 3 - 54   :=  by sorry

Source

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

View graph