Automatically solving olympiad geometry problems

Question

Warning: I am only an amateur in the foundations of mathematics.

My understanding of this Wikipedia page about Tarski's axiomatization of plane geometry (and especially the discussion about decidability) is that "plane geometry is decidable".

The 2019 International Maths Olympiad happened recently, and there were two plane geometry questions in it (problems 2 and 6). Their solutions look really intimidating! However even as a student I felt that one should be able to solve these questions, in theory, by just "writing down coordinates of everything and doing the algebra". Tarski's work, which I will freely confess that I do not understand fully, might even vindicate my view.

The question: Is there an algorithm for solving these kinds of questions, or have I misunderstood? If so, is this algorithm actually feasible to run in practice nowadays (on a computer say) for IMO-level problems? In other words -- are there computer programs which will take as input a planar geometry question of "olympiad level" (for example problems 2 and 6 in this year's IMO) and actually output a solution?

Currently I am not too bothered about whether the solution is human-readable -- it could just be a formal proof in some kind of type theory or something, but the output would be some object that some expert could coherently argue was a solution of some sort.

The reason I'm asking is that I was talking to some computer scientists about various goals in the long-term project of getting computers to do mathematics "better than humans", and having a computer program which could solve IMO problems by itself was a suggested milestone.

Answer 1

Arguably, the so-called "area method" of Chou, Gao and Zhang represents the state of the art in the field of machine proofs of Olympiad-style geometry problems. Their book Machine Proofs in Geometry features over 400 theorems proved by their computer program. Many of the proofs are human-readable, or nearly so.

The area method is less powerful than Tarski–Seidenberg quantifier elimination in the sense that not every statement provable by the latter is provable by the area method, but the area method has the advantage of staying closer to the "synthetic" nature of (the vast majority of) Olympiad problems.

---

EDIT (February 2022): OpenAI has announced some success with solving (some) formal math olympiad problems. They did not restrict themselves to geometry problems.

---

EDIT (January 2024): DeepMind has published Solving olympiad geometry without human demonstrations in Nature. On geometry problems, they claim performance close to that of an Olympiad gold medalist, though I would add some caveats. Their "AlphaGeometry" program does not have natural language processing capability, and is not parsing the Olympiad problem in the natural-language form that a human contestant would be presented with. On 30 selected problems, AlphaGeometry with pre-training and fine-tuning solves 25. They compare this with Wu's method, which they say solves 10 problems. There is no direct comparison with the area method of Chou, Gao, and Zhang, although the line "DD+AR+human-designed heuristics" in Table 1 seems to make some use of the area method, and reportedly solves 18 problems.

Answer 2

There is a pretty general method (although not always sufficient) to apply your intuition that one could translate everything into algebra and then solve it there.

Essentially, you introduce coordinates for your points, encode all your hypothesis as polynomial equalities between coordinates, do the same for the thesis, and then try to prove that the thesis is in the ideal generated by the hypotheses (or even its radical) using Gröbner bases. Of course, the issue here is that the classical Nullstellensatz does not hold for $\mathbb{R}$, so the thesis may hold even if it does not lie in the radical of the ideal generated by the hypotheses. Using the real Nullstellensatz, it may be possible to adapt the technique, but I did not give it much thought.

To make a concrete example, say you want to prove Heron's formula. Let $T$ be a triangle with side length $a, b, c$ and area $s$. You choose coordinates for the vertices of $T$ so that they are $(0, 0), (a, 0), (x, y)$ (this particular nice choice of coordinates is not necessary on a computer but simplifies the discussion for humans). Then the hypotheses are:

• $b^2 = x^2 + y^2$
• $c^2 = (a - x)^2 + y^2$
• $2s = a y$.

The thesis is Heron's formula $16 s^2 = (a + b - c)(c + a - b)(b + c - a)(a + b + c)$.

What you do is consider the ideal $I \subset \mathbb{R}[a, b, c, x, y, s]$ generated by $b^2 - x^2 - y^2$, $c^2 - (a - x)^2 - y^2$ and $2s - ay$, and use Gröbner bases to check that $16 s^2 - (a + b - c)(c + a - b)(b + c - a)(a + b + c) \in \sqrt{I}$.

In fact, since the thesis does not involve $x, y$, one can compute $I \cap \mathbb{R}[a, b, c, s]$ - again using Gröbner bases - and discover that it is generated by the equation expressing Heron's formula.

EDIT

The above can actually be implemented very efficiently. I used rings, an efficient Scala library to perform polynomial computations, and the following

implicit val ring = MultivariateRing(Q, Array("a", "b", "c", "x", "y", "s"))
val h1 = ring("b^2 - x^2 - y^2")
val h2 = ring("c^2 - (a - x)^2 - y^2")
val h3 = ring("2 * s - a * y")
val t = ring("16 * s^2 - (a + b - c) * (c + a - b) * (b + c - a) * (a + b + c)")
val I = Ideal(ring, Seq(h1, h2, h3))
I.contains(t)

gave the answer true is about a second on my laptop.