Prove2Me

lean_workbook_plus_16911

Disproved

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

Show that 3v2+w3<23v^2+w^3<2 if u<3−1u<\sqrt{3}-1, v<3−1v<\sqrt{3}-1, and w<3−1w<\sqrt{3}-1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16911 : ∀ u v w : ℝ, u < (Real.sqrt 3) - 1 ∧ v < (Real.sqrt 3) - 1 ∧ w < (Real.sqrt 3) - 1 → 3 * v ^ 2 + w ^ 3 < 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph