The Tarski-Seidenberg theorem tells us that "semialgebraic" sets in R^n can be projected down to lower dimensions and remain semialgebraic. In practice, this means that one can write an algorithm which takes in any first-order statement about the real numbers (that is, any statement using only the concepts "there exist", "for all", and the operations +, -, *, /, <, =, and, or, not) decides whether or not it is true, and returns a proof of its truth or falsity.

In the LessWrong post which led to the market on AI IMO gold by 2025, one of the first proposed operationalizations of the question of AI performance on the IMO was:

For the 2022, 2023, 2024, or 2025 IMO an AI built before the IMO is able to solve the single hardest problem" where "hardest problem" = "usually problem #6, but use problem #3 instead if either: (i) problem 6 is geo or (ii) problem 3 is combinatorics and problem 6 is algebra.

I suspect the reason why "geo" problems were singled out here, is because most IMOs seem to have a plane Geometry problem which can be formally expressed in the first-order theory of the real by translating statements about points, lines, circles, angles, etc. into statements about algebraic relationships between coordinates of points. These problems can therefore always be solved (in principle) by an AI implementing a quantifier elimination algorithm.

This question asks whether such an algorithm will be a part of the first AI to achieve gold on an IMO. The algorithm must be a subroutine of the AI which is explicitly coded in by a human, rather than being discovered by the AI itself during its development. A human producing the algorithm with the assistance of an AI code generation tool such as codex would count too, as long as the human is describing or guiding the implementation.

Close date updated to 2028-08-10 3:59 pm