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.
1,000
3.00Temporarily closing this question to discuss the 2024 resolution, will reopen afterwards.
I strongly believe 2024 should resolve NO, but I'm happy to wait a few days to discuss arguments in either direction. We're clearly not going to get an official ruling on this, so according to the description I judge this myself. The reason I think this is NO is that AlphaProof took 3 days to find a proof. The spirit of this market is: "does the AI beat all non-bronze medalists of the IMO," and of course giving the AI 3 days means it has an unfair advantage. Now I understand that running time of a computer cluster is somewhat arbitrary, and that with a bigger cluster they could have finished in 9 (or 4.5) hours. But I don't doubt for one second that DeepMind threw a lot of compute at this, and that they really would have liked to be able to say that the AI finished within the competition time. Also, in public presentations DeepMind employees give about this performance, they use the phrase "we achieved silver-level performance", not "we (would've) won a silver medal".
I'm happy to hear counterarguments.
Ping to main 2024 YES holders:
From the description: The years are resolved completely independent of each other.
"Or higher" just means that if AI wins silver or gold, that is also sufficient to resolve a particular year YES.