lean_workbook_plus_79174

Proved

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

Since $Z\ge{2Y^2-Y}$ and $0\le{Y}\le{1}$ , prove: $\frac{2Y^2-Y}{3}+1\ge{\frac{4\sqrt{3}}{9}Y\sqrt{1+2Y}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79174 : ∀ y : ℝ, y ∈ Set.Icc 0 1 → (2 * y ^ 2 - y) / 3 + 1 ≥ (4 * Real.sqrt 3) / 9 * y * (Real.sqrt (1 + 2 * y))   :=  by sorry

Source

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

View graph