lean_workbook_plus_60365

Open

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

Prove that $\cos{3x}=-\frac{1}{2}$ implies $8\cos^3x-6\cos{x}+1=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60365 (x : ℝ) (h : Real.cos (3 * x) = -1 / 2) :
  8 * (Real.cos x)^3 - 6 * Real.cos x + 1 = 0   :=  by sorry

Source