AlphaGeometry solves olympiad geometry problems

Background

The International Mathematical Olympiad (IMO) is the best-known competition for pre-university mathematics. Its problems are built so that a strong school student can in principle solve them with elementary tools, but finding the argument is hard, and only a minority of competitors leave with a medal. Geometry has long been a favourite target for automated reasoning. A geometry problem usually supplies a figure and a claim, and a solution is a chain of logical steps — often with one extra line or circle drawn in that makes the rest fall into place. Strict logic plus one creative step: that mixture is what makes the area a useful test of machine reasoning.

What happened

On 17 January 2024, Google DeepMind announced AlphaGeometry, and published a paper describing the system in Nature ^[1]. The announcement came with a blog post written by Trieu Trinh and Thang Luong ^[1]. The claim DeepMind put forward was a specific one: that this was the first AI model capable of passing the IMO bronze medal threshold as it stood in 2000 and in 2015 ^[1].

How it works

AlphaGeometry paired a language model with a symbolic deduction engine ^[1]. The two components do different jobs, and the design rests on that division. A language model, trained on large amounts of text and other data, is good at proposing plausible next steps, but on its own it does not prove anything: its output is a suggestion, not a guarantee. A symbolic deduction engine works the other way round. It applies formal rules to statements it already holds and derives new statements that follow with certainty, but it can only operate on what it has been given, and it has no sense of which step would be a useful one to try. Put together, the language model contributes candidates and the deduction engine checks and extends them, so that what comes out is a proof rather than a guess ^[1].

Results

The benchmark DeepMind used consisted of 30 olympiad geometry problems, drawn from Olympiads held between 2000 and 2022 ^[1]. AlphaGeometry solved 25 of those 30 within the time limits set for the test ^[1]. The natural yardstick is human: the average gold medallist at the olympiad solved 25.9 of the same problems ^[1].

Those two numbers sit very close together. It is worth being precise about what the comparison does and does not show. AlphaGeometry's 25 is below the 25.9 human average, so the system did not overtake the strongest human solvers on this set. What the result does establish is that a machine system reached roughly the same range as expert competitors on a narrow, well-defined class of problems, with a symbolic engine doing the checking and a learned model supplying the ideas ^[1].

Why it matters

The result matters less as a score than as a demonstration of a way of building systems. Neural models are flexible but unreliable on long chains of exact reasoning; symbolic engines are exact but rigid. AlphaGeometry's contribution is to make each cover the other's weakness, in a domain where correctness can be checked mechanically ^[1]. That is why DeepMind framed it around the olympiad medal thresholds rather than around a generic benchmark: medal thresholds are a familiar, externally defined measure of difficulty, and passing them in the 2000 and 2015 conditions gave the announcement a standard that readers could interpret without knowing the internals of the model ^[1].

The scope should be kept in view. The benchmark was geometry, 30 problems, and the system was measured against one comparison point, the human gold medallist average ^[1]. Geometry is the part of olympiad mathematics where a diagram and formal deduction fit most naturally; other areas of the competition, and problems outside the competition format, are not covered by these numbers. The gap of a fraction of a problem between 25 and 25.9 is also small enough that it should be read as "in the same range", not as a ranking ^[1]. What the announcement established is that the combination of a language model with a symbolic deduction engine could be pushed to olympiad-level geometry, and that the result could be stated in a form — the medal threshold — that anyone who has sat such a competition can judge for themselves ^[1].