lean_workbook_plus_47972

Open

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

Let $ABC$ be an triangle . Prove or disprove that \n $4\cos(\frac {A}{2})\cos(\frac {B}{2})\cos(\frac {C}{2})\ge\sin(A + B + C)$ . \n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47972 (A B C : ℝ) (hx: A > 0 ∧ B > 0 ∧ C > 0) (hab : A + B + C = π) : 4 * Real.cos (A / 2) * Real.cos (B / 2) * Real.cos (C / 2) ≥ Real.sin (A + B + C)   :=  by sorry

Source

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

View graph