Automatically solving olympiad geometry problems

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.

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.