The IMO Grand Challenge aims to “build an AI that can win a gold medal in the (International Mathematical Olympiad) competition.” Geometry problems are an attractive target (e.g., see this MathOverflow discussion or this Lean’s Zulip stream), given the rich literature on automated theorem proving in geometry.

Olympiad participants have long been using well-known computational techniques (i.e., “bashing”) to solve geometry problems, such as complex numbers or barycentric coordinates. How much can we automate these techniques? As a case study, I write programs to solve the two geometry problems in IMO 2019. For this post, I use Maxima, a computer algebra system (easy to install via apt-get on Debian/Ubuntu or Homebrew on macOS). The focus is to explore how to encode these geometry problems such that they can be solved by Maxima within a reasonable amount of time.

NB: I also tried several SMT solvers that support nonlinear real arithmetic. I was able to prove Napoleon’s theorem (the first example below), but not the other two IMO 2019 problems (with a 30-minute timeout). If you have success in finding the right SMT encodings, please let me know!

Complex numbers

There are many good notes on encoding geometry problems using complex numbers. Search for “complex bashing” or refer to Evan Chen’s “Bashing Geometry with Complex Numbers”. The high-level idea is to represent each point with Cartesian coordinate \((x, y)\) as complex number \(z = x + yi\). This often leads to simpler calculation.

The rest of the post uses \(a\) (in lower case) to denote the complex number of the corresponding point \(A\) (in upper case). Below are a few examples.

  • The reflection of point \(A\) over the real axis is: \(\overline{a}\) (i.e., the conjugate of \(a\)).
  • The rotation of point \(A\) about point \(B\) by counterclockwise angle \(\theta\) is: \((a - b) \exp(i\theta) + b\).
  • The centroid of triangle \(ABC\) is: \({(a + b + c)}/{3}\).

See the file geometry.mac for more results (e.g., collinearity, concyclicity, and intersection) coded up in Maxima, which will be used for later proofs.

As a simple example, let’s prove Napoleon’s theorem: the centers of equilateral triangles constructed outward on the sides of a triangle form an equilateral triangle (known as the outer Napoleon triangle).

Let’s do the calculation manually first. \(A, B, C\) are free points.

\(M_1\) is the rotation of \(B\) about \(C\) by \(60\degree\) (i.e., \(\pi/3\)):

\[m_1 = (b - c)\exp(i\pi/3) + c = \dfrac{(\sqrt{3}i + 1)b - (\sqrt{3}i - 1)c}{2}.\]

\(N_1\) is the center (centroid) of equilateral triangle \(M_1BC\), \((m_1 + b + c) / 3\). Therefore, we have:

\[n_1 = \dfrac{(\sqrt{3}i + 3)b - (\sqrt{3}i - 3)c}{6}.\]

Similarly,

\[\begin{aligned} n_2 & = \dfrac{(\sqrt{3}i + 3)c - (\sqrt{3}i - 3)a}{6} \\ n_3 & = \dfrac{(\sqrt{3}i + 3)a - (\sqrt{3}i - 3)b}{6}. \end{aligned}\]

With all the points calculated, it’s straightforward to show that triangle \(N_1N_2N_3\) is equilateral using any of the following encodings for equilaterality:

  • \((n_3 - n_2)\exp(i\pi/3) + n_2 = n_1\),
  • \(\lvert n_1 - n_2\rvert = \lvert n_2 - n_3\rvert = \lvert n_3 - n_1\rvert\),
  • \(n_1^2 + n_2^2 + n_3^2 = n_1n_2 + n_2n_3 + n_3n_1\) (see proof).

Now let’s automate the calculation using the following Maxima program:

load("geometry.mac");
  
/* Declare triangle ABC. */
declare([a, b, c], complex);

/* Compute the outer Napoleon triangle. */
p(x, y) := centroid(x, y, rotate(x, y, %pi/3));
[n1, n2, n3] : [p(b, c), p(c, a), p(a, b)];

/* Prove that the outer Napoleon triangle is equilateral. */
prove(equilateral(n1, n2, n3));

quit();

The prove function (defined in geometry.mac) calls Maxima’s built-in is function to determine whether a predicate is provably true. Below is the execution trace of this program:

% maxima -b napoleon.mac
Maxima 5.44.0 http://maxima.sourceforge.net
using Lisp SBCL 2.0.5
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
The function bug_report() provides bug reporting information.
(%i1) batch("napoleon.mac")

read and interpret napoleon.mac
(%i2) load("geometry.mac")
(%o2)                             geometry.mac
(%i3) declare([a,b,c],complex)
(%o3)                                done
(%i4) p(x,y):=centroid(x,y,rotate(x,y,%pi/3))
                                                        %pi
(%o4)            p(x, y) := centroid(x, y, rotate(x, y, ---))
                                                         3
(%i5) [n1,n2,n3]:[p(b,c),p(c,a),p(a,b)]
              sqrt(3) %i   1                sqrt(3) %i   1
       2 c + (---------- + -) (b - c) + b  (---------- + -) (c - a) + c + 2 a
                  2        2                    2        2
(%o5) [----------------------------------, ----------------------------------, 
                       3                                   3
                                                   sqrt(3) %i   1
                                            2 b + (---------- + -) (a - b) + a
                                                       2        2
                                            ----------------------------------]
                                                            3
(%i6) prove(equilateral(n1,n2,n3))
(%o6)                                true
(%i7) quit()

If we attempt to prove something false, such as \(N_1N_2C\) equilateral, the execution fails:

(%i6) prove(equilateral(n1,n2,c))
prove(equilateral(n1,n2,c))
Unable to evaluate predicate errexp1
...
 -- an error. To debug this try: debugmode(true);

Exercise 1: Extend the above program to prove that the center of the outer Napoleon triangle \(N_1N_2N_3\) corresponds to the centroid of triangle \(ABC\).

Exercise 2: Prove Napoleon’s theorem using an SMT solver or Gröbner bases.

  • For SMT, you may find Leonardo de Moura’s “Complex Numbers in Z3” useful. To make the code work in Python 3, change __div__ to __truediv__ and __rdiv__ to __rtruediv__.

  • For Gröbner bases, you may find Dan Roozemond’s “Gröbner Bases in Practice” chapter useful. The paper uses the Singular computer algebra system. Maxima and SymPy should also work.

IMO 2019, problem 2

In triangle \(ABC\), point \(A_1\) lies on side \(BC\) and point \(B_1\) lies on side \(AC\). Let \(P\) and \(Q\) be points on segments \(AA_1\) and \(BB_1\), respectively, such that \(PQ\) is parallel to \(AB\). Let \(P_1\) be a point on line \(PB_1\), such that \(B_1\) lies strictly between \(P\) and \(P_1\), and \(\angle PP_1C = \angle BAC\). Similarly, let \(Q_1\) be a point on line \(QA_1\), such that \(A_1\) lies strictly between \(Q\) and \(Q_1\), and \(\angle CQ_1Q = \angle CBA\).

Prove that points \(P\), \(Q\), \(P_1\), and \(Q_1\) are concyclic.

See the solution in Maxima imo2019p2.mac.

Here’s the high-level flow. \(A, B, C\) are free points, from which we derive \(A_1\) and \(B_1\). We derive \(P\) and \(Q\) by introducing another free point \(K\), the line through which parallel to \(AB\) intersects \(AA_1\) and \(BB_1\) at \(P\) and \(Q\), respectively. The remaining question is how to encode \(P_1\) and \(Q_1\).

First, \(P_1\) on \(PB_1\) may translate to:

\[\frac{p_1 - b_1}{b_1 - p} = \overline{\left(\frac{p_1 - b_1}{b_1 - p}\right)}.\]

\(\angle PP_1C = \angle BAC\) may translate to:

\[\frac{p_1 - c}{p_1 - p} / \frac{a - c}{a - b} = \overline{\left(\frac{p_1 - c}{p_1 - p} / \frac{a - c}{a - b}\right)}.\]

Since \(a, b, c, p\) are known at this point, one may solve \(p_1\) by eliminating \(\overline{p_1}\) from the above two equations (by hand or using Maxima’s solve function). One may solve \(q_1\) similarly.

Next, it’s straightforward to prove that \(P, Q, P_1, Q_1\) are concyclic by testing the following:

\[\frac{p_1 - p}{p_1 - q} / \frac{q_1 - p}{q_1 - q} = \overline{\left(\frac{p_1 - p}{p_1 - q} / \frac{q_1 - p}{q_1 - q}\right)}.\]

Maxima reported the following error on my first attempt:

PQUOTIENT: Quotient by a polynomial of higher degree (case 2b)
 -- an error. To debug this try: debugmode(true);

I worked around this error by choosing \(C\) as the origin (i.e., \(c = 0\)), with which Maxima is able to finish the proof.

Notice that the problem description is not constructive: it asserts the existence of points \(P_1\) and \(Q_1\) but doesn’t say how to construct them—imagine how to draw the figure without solving polynomials. Below is one way to rephrase the problem (in fact, that’s how I drew the above figure), inspired by “solution 1” of this problem’s reference solutions.

Problem 2*: Points \(A_2\) and \(B_2\) are on the circumcircle of triangle \(ABC\). \(AA_2\) intersects \(BC\) at \(A_1\). \(BB_2\) intersects \(CA\) at \(B_1\). Let \(P\) and \(Q\) be points on segments \(AA_1\) and \(BB_1\), respectively, such that \(PQ\) is parallel to \(AB\). \(PB_1\) intersects the circumcircle of triangle \(CB_1B_2\) again at \(P_1\). \(QA_1\) intersects the circumcircle of triangle \(CA_1A_2\) again at \(Q_1\).

Prove that points \(A_2, B_2, P, Q, P_1, Q_1\) are concyclic.

It’s easy to see that this constructive version is equivalent to the original problem, given \(\angle PP_1C = \angle B_1B_2C = \angle CAB\) and \(\angle QQ_1C = \angle A_1A_2C = \angle CBA\).

Exercise 3: Write a Maxima program to prove problem 2*.

IMO 2019, problem 6

Let \(I\) be the incenter of acute triangle \(ABC\) with \(AB \neq AC\). The incircle \(\omega\) of \(ABC\) is tangent to sides \(BC\), \(CA\), and \(AB\) at \(D\), \(E\), and \(F\), respectively. The line through \(D\) perpendicular to \(EF\) meets \(\omega\) again at \(R\). Line \(AR\) meets \(\omega\) again at \(P\). The circumcircles of triangles \(PCE\) and \(PBF\) meet again at \(Q\).

Prove that lines \(DI\) and \(PQ\) meet on the line through \(A\) perpendicular to \(AI\).

See the solution in Maxima imo2019p6.mac.

The problem description is constructive, and it’s fairly straightforward to calculate each point. Two optimizations are worth mentioning.

First, to avoid calculating the incenter, a standard approach is to choose \(I\) as the origin and \(D, E, F\) as points on a unit circle. Let’s introduce angle \(\theta_d\) such that \(D\) is \(\exp(i\theta_d)\); \(E\) and \(F\) are calculated similarly. The rest of the points can be derived from \(D, E, F\).

Second, choose \(IA\) as the real axis (i.e., \(\theta_f = -\theta_e\)), which exploits the symmetry of \(E\) and \(F\). Without this optimization, the program timed out (in 30 minutes).

One may notice the complexity in calculating \(L\), the intersection of \(DI\) and \(PQ\), which is due to the complexity in \(P\) and \(Q\). One possible optimization to calculate \(L\) from points with simpler coordinates, \(DI\) and the line through \(A\) perpendicular to \(AI\), and instead prove that \(P, Q, L\) are collinear.

Exercise 4: Optimize the Maxima code using the above approach.

Summary

Below is a list of the Maxima files used in this post.

The proofs described in this post are close to those written by hand using complex numbers. The optimizations are fairly standard, such as choosing a point as the origin or choosing the real axis to exploit symmetry, which might be possible to automate in the future.

The IMO Grand Challenge expects an AI to produce mechanical proofs that can be checked by the Lean theorem prover. Some of the other IMO 2019 problems are already formalized in Lean (e.g., problem 1 by Kevin Buzzard and problem 4 by Floris van Doorn). Maxima doesn’t produce Lean-checkable proofs, so it requires further work (e.g., building on efforts such as GeoCoq). Another important factor is how these problems will be encoded formally.

Acknowledgments: Luke Nelson, Emina Torlak, and Zhilei Xu provided feedback on a draft of this post.