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:

• Update 2025-01-01 (PST) (AI summary of creator comment): - The AI's computation time to produce a proof will be considered in determining if it had an unfair advantage.

  • If the AI requires significantly more time than typical competition time (e.g., taking several days), it may influence the resolution to NO.