Prove2Me

lean_workbook_plus_70599

Proved

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

x3+133+133≥x⇒x(1−x2)≤233 x^3+\frac{1}{3\sqrt{3}}+\frac{1}{3\sqrt{3}}\geq x\Rightarrow x(1-x^2)\leq\frac{2}{3\sqrt{3}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70599 (x : ℝ) : x^3 + 1 / (3 * Real.sqrt 3) + 1 / (3 * Real.sqrt 3) ≥ x → x * (1 - x^2) ≤ 2 / (3 * Real.sqrt 3)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph