Now that 2023 has come and gone with no IMO claims, I am putting a limit order on NO 2023 at 1% in case there were people whose loans have not vested and want to get out at that price.

In the spirit of sharing one's beliefs:

The 3% on 2023 seems too high to me: it requires that some relevant entity aimed for IMO gold *and* they succeeded (meaning a huge increase in AI math capabilities) *and* such a model has existed for over a month but it's not publicly known.

I think the combination of the first two is quite unlikely, even given that they are not independent. Taking the conjunction with the third statement puts the probability below 3% for me.

Regarding the other years: I think the main market (https://manifold.markets/Austin/will-an-ai-get-gold-on-any-internat), currently at 31%, is too high (and I've been betting NO on it). This market's 7%+17%=24% for 2024-2025 seems reasonable to me. For later years I have no strong opinions - long-term future forecasts are hard, doubly so in AI - and have not bet on them.

@Loppukilpailija I think the last condition of your 2023 decomposition is not necessarily necessary. If an LLM for which dataset collection finished in say May 2023, but training finishes in November 2023, achieves gold on this year's IMO (so on IMO whose problems were not in its training set), my impression is that that would probably count as gold in 2023 by judgment of Christiano/Yudkowsky.

Yudkowsky's quote from the bet post which I think supports this kind of pragmatism:
> I see they want to demand that the AI be open-sourced publicly before the first day of the IMO, which unfortunately sounds like the sort of foolish little real-world obstacle which can prevent a proposition like this from being judged true even where the technical capability exists.  I'll stand by a >16% probability of the technical capability existing by end of 2025

@Lovre The original blog post was sparked by the IMO grand challenge, which is a challenge to write an AI that produces machine-checkable proofs. The IMO grand challenge indeed requires the program to be open source.

However, Paul Christiano has clarified in a comment on the main market that he will concede the bet if the AI produces a natural language proof, no need for it to be machine-checked. Since he is being more liberal with the conditions, I'm almost sure that he will concede the bet even if the AI is not open source.

@Lovre I indeed did not think of the scenario "the code has already been written before the IMO, but the model is still being trained". I don't think that's particularly likely, but it makes me a bit less confident in that the year cannot be 2023.

relevant individual markets:
(note that all the "by"'s are inclusive, except maybe for the 2032 market)

https://manifold.markets/BoltonBailey/will-an-ai-get-gold-on-any-internat-2b53f4a252d8#wRwN6ej6uONGMXD9IjMN and https://manifold.markets/Austin/will-an-ai-get-gold-on-any-internat are currently at 9% and 39%, which means that 2025 should have 30% probability. Who wants to arbitrage with the current 17% on this market?

I made a version of this market specifically for the (formalized) IMO grand challenge:

I'm avoiding trading but note that the market linked in the description is at 38% now, while the probabilities here would imply 26%.

@BoltonBailey I've moved the timelines up for this reason. I think the Metaculus one is slightly unreliable as around 10% of the probability mass is in the past.

I just made a bunch of trades to basically bring this market to a very similar distribution to this Metaculus question: https://www.metaculus.com/questions/6728/ai-wins-imo-gold-medal/

When will an AI win a Gold Medal in the International Math Olympiad?

The aggregate of 192 Metaculus community forecasters was Jan 16, 2028 on Jun 25, 2023.

@jacksonpolack If you shorted 2024 here, you might be interested in shorting this one too

Will an AI get gold on any International Math Olympiad by 2024?

10% chance. Same as this market, but for AI that gets gold on the 2023 or 2024 IMO.