Prove2Me

lean_workbook_plus_29517

Disproved

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

or 4sqrt(u2−v2)3leq5u3−4uv2−uvsqrt9u2−8v24\\sqrt{(u^2-v^2)^3}\\leq 5u^3-4uv^2-uv\\sqrt{9u^2-8v^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29517 :  ∀ u v : ℝ, 4 * Real.sqrt ((u ^ 2 - v ^ 2) ^ 3) ≤ 5 * u ^ 3 - 4 * u * v ^ 2 - u * v * Real.sqrt (9 * u ^ 2 - 8 * v ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph