I'm surprised/skeptical of the implied ~70% probability of both of the underlyings resolving YES. Before the AlphaProof news there was a 50% chance of this market resolving YES, now learning about AlphaProof from DeepMind causes the market to think it's even more likely that multiple groups will medal?

Perhaps people expect that AlphaGeometry or AlphaProof could be separately counted for the Bronze/Silver market and AlphaProof+AlphaGeometry for the Gold?

@BoltonBailey See now this new market for potential arbs

What are the resolution criteria here? The marked referred to in the description refers to gold, so presumably it does not suffice for YES resolution based on "at least bronze," and the other market has no resolution criteria of its own either.

There's two linked markets. Unfortunately the bronze silver one is underspecified (unclear if formal counts)

@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.)

https://manifold.markets/market/will-an-ai-get-gold-on-any-internat?tab=comments#Sj3pX2yIgHTnVH2PyX2Y

But maybe you should ask Paul Christiano whether he would accept a gold score if it took 3 days to find it. I think there are reasonable arguments on both sides of that question.

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.

Does "by 2025" mean "by the start of 2025" or "by the end of 2025"?

@rogs End of 2025, I think.

the thing for these AIMO markets, we need a certified grader to grade the AI

I made two related markets:

Related: https://manifold.markets/dp/what-imo-shortlist-topic-acn-will-b

When I saw the DeepMind paper, I knew that if I went to Manifold there would be free mana waiting for me on some market and lo and behold.

Spike from deepmind getting in between IMO silver and gold performance on geometry problems

limit order at 30% if someone wants to take it

Real incentive: $10M prize for IMO gold just announced. https://aimoprize.com/

@RjieRieisi