# Commit 2020-10-13 02:01 7dcaee1c

View on Github →feat(archive/imo): formalize IMO 1962 problem 4 (#4518)
The problem statement: Solve the equation `cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1`

.
There are a bunch of trig formulas I proved along the way; there are sort of an infinite number of trig formulas so I'm open to feedback on whether some should go in the core libraries. Also possibly some of them have a shorter proof that would render the lemma unnecessary.
For what it's worth, the actual method of solution is not how a human would do it; a more intuitive human method is to simplify in terms of `cos x`

and then solve, but I think this is simpler in Lean because it doesn't rely on solving `cos x = y`

for several different `y`

.