How AlphaGeometry Combines Logical Proof with Creative Construction

In January 2024, Google DeepMind released AlphaGeometry, a system that could solve geometry problems from the International Mathematical Olympiad, or IMO. This is the highest level of international mathematics competition for high-school students. More than 100 countries each send six teenagers, selected through their own elaborate series of competitions. On a test set of 30 geometry problems, AlphaGeometry solved 25, surpassing the performance associated with a silver medalist.

For me, the most surprising part is what happened before the AI entered the picture. Techniques based on logic and equation solving already handled a remarkable number of these problems. But they eventually hit a wall: there were problems their logical machinery could not solve. Instead of asking AI to do everything, the DeepMind team combined that machinery with a learned component. I want to explain both halves, beginning with what a system can accomplish without AI.

Our task is to build a bot that solves IMO geometry problems, with the extra restriction that it cannot use AI. A useful secret about geometry is that a few key facts can take you surprisingly far. When two lines cross, vertically opposite angles are equal. When a transversal crosses parallel lines, the alternate interior angles—the angles inside a Z shape—are equal. Applying just these two facts in succession already proves a nontrivial statement about the diagram.

Now imagine starting with 10 facts, or 50, or 100. The collection of theorems you could prove would grow as those facts combined in different ways. A paper published in October 2000 took this approach with a database of 75 geometry rules. Some are elementary, like the rules we have just used; others are more elaborate. Repeatedly applying them let the researchers solve some very difficult geometry problems.

The computer still needs a way to represent a geometry problem. One option would be to place everything in coordinates and write explicit equations, but that is cumbersome. Another is a theorem-proving language such as Lean. While Lean is powerful for areas such as algebra and inequalities, the approach described here uses a more specialized language designed for Euclidean geometry. At the time of this account, I do not know of an official name for it beyond its descriptions in research papers.

Consider the statement that a triangle with two equal sides has two equal angles. In this geometry language, we declare three points, A, B, and C; state that AB = AC; and specify the goal that angle ABC equals angle BCA. The researchers call the method a deductive database, or DD. The database supplies the starting facts, and deduction produces further consequences from them.

On the 30-problem IMO geometry test set, DD solved seven problems. You can look at that in two ways. Seven out of 30 is far from an outstanding Olympiad score. Yet these are very hard problems, and getting even one solution from a brute-force application of geometric rules is impressive. Before concluding that AI is the only way to improve the result, we should address a basic limitation: DD cannot solve equations.

Thales’ theorem gives a simple illustration. An angle subtended by a diameter of a circle is a right angle. To prove it, connect the third point on the circle to the center. The resulting three radii have equal lengths, so the two smaller triangles are isosceles. Their equal base angles can be labeled alpha and beta. Because the large triangle’s angles sum to 180 degrees, we obtain 2 alpha + 2 beta = 180 degrees.

Dividing that equation by two gives alpha + beta = 90 degrees. Those two angles together make the angle at B, so the proof is complete. This final algebraic manipulation is easy for a computer equipped with linear algebra, but it is a capability the deductive database lacks. The DeepMind researchers added a module called algebraic reasoning, or AR, to solve systems of linear equations.

We now have two modules: DD applies a hard-coded list of geometric rules, while AR solves the equations that arise. The system alternates between them. It runs DD until deduction stops producing progress, then AR until that stops, and then returns to DD. It repeats until it proves the desired statement or runs out of time. The combined procedure is called DD + AR.

In one example from the paper, geometric deduction produces two relationships, and algebraic reasoning solves the resulting equations. The benchmark results show the value of this combination. DD alone solves seven of 30 problems; DD + AR solves 14. Adding human-coded heuristics increases the number to 18, close to bronze-medal performance. I find it remarkable that a largely brute-force approach can go so far on problems as hard as IMO geometry.

If we can do all that without AI, why add it? The remaining weakness is auxiliary constructions. To solve many geometry problems, you must draw extra lines or shapes that are not already present. The existing diagram may contain everything needed to state the problem, yet leave out exactly the construction that makes the proof possible.

Take the theorem that a triangle’s angles sum to 180 degrees. Draw parallel lines through the top and bottom of the triangle. Alternate interior angles identify one angle with alpha and another with beta; call the remaining angle gamma. Along the straight line at the top, alpha + gamma + beta = 180 degrees. Because these are also the triangle’s three angles, the result follows.

The crucial step was drawing those lines. After that, familiar facts supplied the proof. This is part of what makes geometry enjoyable: the right extra idea can seem to come from nowhere. An IMO problem may require several such constructions. For a machine, that means confronting an infinite space of possible additions at each step, something our purely deductive engine is poorly suited to search.

The DeepMind team built a language model with one specific job: propose auxiliary constructions. Its input is the problem statement together with the proof steps generated so far. Although I am describing these in English, the system receives them in the specialized geometry language. Its output is a construction, such as an extra point or figure to add to the diagram.

The full AlphaGeometry loop begins by giving the problem to the language model and receiving a proposed construction. The expanded diagram goes to DD + AR, which derives as much as it can. Those deductions return to the language model, which proposes another construction. The process continues, alternating new ideas with logical consequences, until the problem is solved or time runs out.

One way to picture the partnership is as a creative brain and a logical brain. The language model comes up with a potentially useful addition. DD + AR uses known rules and equations to determine what follows from it. Then the model supplies another idea, and the logical engine derives more consequences. The learned component guides the search while the symbolic component carries out the reasoning.

That leaves a major question: where does the language model get its training data? There are not enough published IMO geometry problems and solutions to train such a model directly. The AlphaGeometry team sidestepped the shortage by generating its own examples. Begin by randomly plotting points and lines, then use DD + AR to derive everything possible from the resulting diagram.

Suppose those deductions establish that a triangle’s angles sum to 180 degrees. We can work backwards and erase some of the lines from the diagram. The remaining figure now defines a problem: given this triangle, prove the angle sum. Solving it requires redrawing the erased lines as auxiliary constructions. Repeating this procedure turns randomly generated diagrams and their deductions into training problems with known construction steps.

The researchers generated hundreds of millions of synthetic proof examples. Nine million required at least one auxiliary construction. Some of the resulting diagrams are extremely complicated; the longest synthetic proof described here contains 247 steps and uses two auxiliary constructions. These examples supplied the data needed to train the language model.

The performance progression is striking. DD solves seven of 30 problems, DD + AR solves 14, and the version with human-coded heuristics solves 18. Combining DD + AR with the trained language model, including fine-tuning, raises the result to 25 of 30. The learned component helps the symbolic engine reach proofs it could not find on its own.

To me, the exciting part is about more than triangles. AlphaGeometry brings creative suggestions together with logical reasoning. That partnership is familiar in human problem solving across science, medicine, and engineering. The system itself was not built to solve problems in those other fields, but it offers a glimpse of a general strategy machines might use: invent a useful idea, work out its consequences, and repeat.

The closing introduction identifies this lesson as the second in 3Blue1Brown’s summer guest-video series, made by the creator of Aleph0. The channel is recommended for its concise but substantial explanations of higher-level mathematics.