Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1962P4

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

/-!
# International Mathematics Olympiad 1962, Problem 4

Solve the equation
     cos² x + cos² (2 * x) + cos² (3 * x) = 1.
-/

open Real

namespace Imo1962P4

def ProblemEquation (x : ℝ) : Prop :=
  cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1

/- determine -/ abbrev solutionSet : Set ℝ := sorry

theorem imo1962_p4 {x : ℝ} : ProblemEquation x ↔ x ∈ solutionSet := sorry


end Imo1962P4

File author(s): Kevin Lacker, Heather Macbeth

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo1962Q4.lean.