This market resolves based off the outcomes of two other markets:
If either of these resolve YES, this resolves YES. If both resolve NO, this resolves NO. If either of the linked markets resolves to something other than YES or NO, I will use my best judgement.
Apr 29, 9:01pm: Will AI get at least Bronze on the IMO by 2025? → Will AI get at least bronze on the IMO by 2025?
Related questions
@jack yes, those are the markets I was referring to. There is a lot of underspecification at play here.
I am noticing that somewhat contradictory statements have been made about formal-to-formal. IMO Grand Challenge, as articulated on its website, is about formal to formal. But I'm pretty sure Paul Christiano has said that the market is just about how he and Eliezer Yudkowsky will resolve their bet and informal to informal would count for that too as well as F2F. The quoted post mentions the IMO Grand challenge and the question has the IMO Grand Challenge tag, but I'm pretty sure it only has the tag because I added it myself.
In the main market Paul Christiano wrote this:
> The bet is about what I and Eliezer will say. I will concede the bet if an AI produces natural language proofs that receive a gold using normal human scoring, no need to give fully formal proofs. (I will also concede if the AI gives a formal proof given a formal statement, no need to deal with natural language.)
I think getting a medal on the IMO implies competing at similar conditions to participants. Otherwise, I too have gold on IMO.
Current results were manually translated by humans, were not time restricted, were not graded by same evaluators. Google ran their software on IMO questions ≠ google won a medal on IMO, despite what the headlines would lead to believe.
>I think getting a medal on the IMO implies competing at similar conditions to participants.
This.
limit order at 30% if someone wants to take it