[tsimionescu]

AlphaGeometry works, in simplified terms, in two stages:

1. Heuristically add a candidate construction using an NN (a transformer)

2. Brute force search through all possible deductions from the current set of constructions using a symbolic solver

If you don't find a solution after step 2, repeat. There may be some backtracking involved to try a different set of constructions as well.

This approach only works because, in geometry, the set of possible deductions from a given construction is actually quite small.

Also, note that this approach overall is essentially an optimization, not amazing new capabilities. Replacing step 1 with a random construction still solves 10 problems on average in the given time, compared to 30 with the new approach. The existing algorithm, relying mostly on brute force search, is probably able to solve all of the geometry problems if given, say, 10 times as much time as the olympiad students (so not some absurd amount of time).