Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1963P5

import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Data.Real.Pi.Bounds

/-!
# International Mathematical Olympiad 1963, Problem 5

Prove that cos(π/7) - cos(2π/7) + cos(3π/7) = 1/2.
-/

namespace Imo1963P5

open scoped Real

theorem imo1963_p5 :
    Real.cos (π/7) - Real.cos (2*π/7) + Real.cos (3*π/7) = 1/2 := sorry
end Imo1963P5

File author(s): Hongyu Ouyang

This problem has a complete formalized solution.