Prove2Me

lean_workbook_plus_12199

Proved

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

Proof for a2(1−a)≤427 a^{2}(1-a)\le\frac{4}{27} . If 1−a<0 1-a<0 , the inequality is obvious. Otherwise, (2−2a)+a+a3≥2(1−a)(a)(a)3 \frac{ (2-2a)+a+a}{3}\ge\sqrt[3]{2(1-a)(a)(a)} , as desired.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12199  (a : ℝ)
  (h₀ : 0 ≤ a)
  (h₁ : a ≤ 1) :
  a^2 * (1 - a) ≤ (4:ℝ) / 27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph