[Merged by Bors] - feat(archive/imo): formalize IMO 1962 problem 4

[lacker]

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.

[PatrickMassot]

Suggested change

	have h1 : x + 2 * x = 3 * x, by ring,
	rw [← h1, cosh_add x (2 * x)],
	rw [show 3*x = x + 2*x, by ring, cosh_add x (2 * x)],

and you can do it in many other places.

[lacker]

To me this just seems like making it less readable in order to squish two lines into one. It isn't making the proof any simpler. I'd rather keep it as is.

[hrmacbeth]

I would like to propose some changes to the structure of the proof, with the idea of separating out the different kinds of arguments that occur.

Idea 1: factor out the pure algebraic lemma that a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1 if and only if (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0. This lemma is a little nontrivial, since a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1 is directly equivalent to a * (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0, so to cancel the a factor you have to notice the presence of a second a factor in the third term. If this step were being automated, it would be by showing that the ideals generated by the two expressions have the same Jacobson radical.

Then, prove that problem_equation if and only if cos (2 * x) = 0 or cos (3 * x) = 0, by simping using the algebraic equation, cos_two_mul, cos_three_mul, and the field_simp simp set.

Idea 2: replace solve_cos2_half with solve_cos2x_0, which can have the exact same proof as your lemma solve_cos3x_0. (Maybe even prove an n-version and deduce both from this.)

[lacker]

I would like to propose some changes to the structure of the proof, with the idea of separating out the different kinds of arguments that occur.

I think the ideal method of proof would actually be different from all of these. It would be to first simplify the equation in terms of cos x, because intuitively cos (2 * x) and cos (3 * x) are ugly. Then notice that it's a polynomial in cos x ^ 2, and then to use standard polynomial methods to solve. I find using the cos (3 * x) term to be quite unnatural. However, I was getting bogged down in the huge amount of basic stuff that needed to be added to the trig libraries to do it the intuitive way, and this was a shortcut. In particular, we have no convenient way to solve basic middle school stuff like solving cos x = sqrt(3)/2.

So for this pull request, I would like to just leave it as is, since it's reasonably close to a human method.

[hrmacbeth]

On the one hand, I think that relying on the coincidence of the cos (3 * x) term appearing is not so unnatural. That's because coincidences are actually necessary in order for the equation P (cos x) = 0 (where P is a polynomial) to have "nice" IMO-friendly solutions -- otherwise the solution set would just be something like {x | ∃ k : ℤ, x = 2 * k * π + arccos a} where a is some random algebraic number.

On the other hand, I think it's reasonable to aim for a human-like solution to this problem. But could you please take it a step further in this direction? I think you could add the lemma cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x and the lemma cos (π / 6) = (sqrt 3) / 2, then you'd be effectively done with this:

However, I was getting bogged down in the huge amount of basic stuff that needed to be added to the trig libraries to do it the intuitive way, and this was a shortcut. In particular, we have no convenient way to solve basic middle school stuff like solving cos x = sqrt(3)/2.

Am I overlooking something?

[lacker]

Honestly, I'm sick of adding new lemmas to make this proof a small fraction more aesthetically pleasing. This pull request is already adding 20 new lemmas to mathlib. Can't we just check it in?

[hrmacbeth]

If you don't mind me pushing to your branch, I can do this myself later tonight. Your frustration is fair, it's just that every time you PR a problem we see it as a test case to make the next ten similar problems easier!

[lacker]

Why don't we check this in, and then you can just push your improvements to master?

[lacker]

(But if you insist, yes please go ahead and push to my branch.)

[hrmacbeth]

Why don't we check this in, and then you can just push your improvements to master?

OK, fair enough, let me just ping another maintainer to second-opinion this.

In the meantime there were a couple of points I didn't mention in the first review because they were on code I thought would be refactored -- I'll run through them now.

[hrmacbeth]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests