A year resolves yes, if any AI program can get enough points to win at least bronze on the International Mathematics Olympiad of that year. The years are resolved completely independent of each other.

If a neutral party (e.g. from the AIMO prize) judges AI performance in this respect, I will defer to them. Otherwise, I will judge myself.

If I judge, my main requirements are that the AI was written and trained (if applicable) before the IMO, though it need not be released before the IMO.

The AI should produce a proof that can be checked within a reasonable time by either a human or a proof assistant (e.g. Lean). I will wait a while after the IMO before resolving each year.

I will not bet on this market.

Related questions: