Prove2Me

lean_workbook_plus_14729

Open

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

P=94−4(sin⁡A2−14)2≤94P=\frac{9}{4}-4(\sin{\frac{A}{2}}-\frac{1}{4})^{2}\leq\frac{9}{4}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14729 : ∀ A : ℝ, (9 / 4 - 4 * (Real.sin (A / 2) - 1 / 4) ^ 2) ≤ 9 / 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph