lean_workbook_plus_78015

Open

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

If $\cos \alpha=\frac{60} {61}, 0\le \alpha \le \frac{\pi} {2}$ , find the exact value of $\sin{\frac{\alpha} {2}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78015 (α : ℝ) (h₁ : 0 ≤ α) (h₂ : α ≤ π/2) (h₃ : cos α = 60/61) : sin (α/2) = √122 / 122   :=  by sorry

Source