lean_workbook_plus_17202

Proved

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

Somehow, using calculus to maximize a quadratic always strikes me as overkill. You could just complete the square. Or use AM-GM: For $x>0$ and $1-x>0,$ $\sqrt{x(1-x)}\le\frac12(x+(1-x))=\frac12.$ Hence $x(1-x)\le\frac14,$ with equality when $x=1-x.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17202  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : x < 1) :
  x * (1 - x) ≤ 1 / 4   :=  by sorry

Source

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

View graph