The fourth question on this year’s IMO is a Euclidean geometry question. And so I thought to myself, I wonder if I could get a computer algebra package (with Grobner bases, etc) to do the relevant algebraic manipulation to solve the problem for me, once I had converted the problem into coordinate geometry.

This is a desription of that journey. But first the problem:

Points P and Q lie on side BC of acute-angled triangle ABC such that and . Points M and N lie on lines AP and AQ, respectively, such that P is the midpoint of AM and Q is the midpoint of AN. Prove that the lines BM and CN intersect on the circumcircle of triangle ABC.

As every good student knows, it is a good idea to do a little bit of Euclidean geometry before starting on the trigonometry or coordinate geometry. So we will begin by noticing that APQ is isosceles.

We will set up our coordinates so that the line BC is the horizontal axis, with the origin at the midpoint of PQ. Then we introduce variables by , , , and . Hence and .

Let be the intersection of BM and CN and let be the circumcentre of ABC.

So now for the equations that these seven variables satisfy.

Since X lies on BM, there is

and since X also lies on CN, there is

From |AO|=|BO| there is

and from the similarity of triangles ABC and QAC, in particular , we get

And what do we have to prove? Well nothing other than |AO|=|XO|, so it suffices to prove

So, we go to `sage`

(I skip the routine and boring simplification) and execute

`sage: x,h,y,z,w,p,q=QQ['x,h,y,z,w,p,q'].gens()`

sage: I=ideal(q*(2*x-y)+h*(p-y),q*(2*x+z)-h*(p-z),y*z-2*w*h+h^2,h^2+z^2-(z+x)*(z-y))

sage: (p^2-p*y-p*z+(q-w)^2-(w-h)^2) in I

False

Yikes!

Well how about:

`sage: (p^2-p*y-p*z+(q-w)^2-(w-h)^2) in I.radical()`

False

Yikes again!

While it is tempting to expect a typographical error, that is not in fact the case. The following computation reveals what is really going on.

`sage: I.associated_primes()`

[Ideal (q, z, y, h) of Multivariate Polynomial Ring in x, h, y, z, w, p, q over Rational Field, Ideal (q, z, h, x) of Multivariate Polynomial Ring in x, h, y, z, w, p, q over Rational Field, Ideal (q, y, h, x) of Multivariate Polynomial Ring in x, h, y, z, w, p, q over Rational Field, Ideal (z, y, h, x) of Multivariate Polynomial Ring in x, h, y, z, w, p, q over Rational Field, Ideal (y*p + z*p - 2*p^2 - 2*h*q + 4*w*q - 2*q^2, y*z - p^2 - 2*h*q + 2*w*q - q^2, h*z - h*p + 2*x*q + z*q, 2*x*z - 2*h*w - 2*x*p - z*p + p^2 + h*q - 2*w*q + q^2, h*y - h*p - 2*x*q + y*q, 2*x*y + 2*h*w - 2*x*p - z*p + p^2 + h*q - 2*w*q + q^2, h^2 - 2*h*w + p^2 + 2*h*q - 2*w*q + q^2, z*p^2 - p^3 - 2*x*h*q + 4*x*w*q - h*p*q + 2*w*p*q - 2*x*q^2 - p*q^2, z^2*p - p^3 - 4*x*h*q + 8*x*w*q + 4*z*w*q - 2*h*p*q + 2*w*p*q - p*q^2, 2*h*w^2 - w*p^2 + 2*x^2*q - h*w*q + 2*w^2*q - w*q^2, h*w*p^2 - 2*x^2*h*q + 4*x^2*w*q - 2*x^2*q^2, w*p^4 - 4*x^2*h*w*q + 8*x^2*w^2*q - 2*x^2*p^2*q - 2*w^2*p^2*q + 2*x^2*h*q^2 - 8*x^2*w*q^2 + w*p^2*q^2 + 2*x^2*q^3) of Multivariate Polynomial Ring in x, h, y, z, w, p, q over Rational Field]

And we see the issue. The ideal I has five associated primes, but only one of these primes corresponds to the geometric problem at hand, the other four correspond to highly degenerate triangles.

So we try

sage: J=I.associated_primes()[4]

sage: (p^2-p*y-p*z+(q-w)^2-(w-h)^2) in J

True

and the proof is complete.

An alternative approach would be to artificially invert by creating a new variable satisfying the relation :

sage: x,h,y,z,w,p,q,t=QQ['x,h,y,z,w,p,q,t'].gens()

sage: I=ideal(q*(2*x-y)+h*(p-y),q*(2*x+z)-h*(p-z),y*z-2*w*h+h^2,h^2+z^2-(z+x)*(z-y),h*t-1)

sage: (p^2-p*y-p*z+(q-w)^2-(w-h)^2) in I

True

and QED for the second time.