Oh no this won’t happen idk what past me was thinking

(to clarify: they'll get gold, and nobody will report the shame of only getting silver)

@Bayesian I mean, DeepMind already reported having their AI win silver, with only 1-2 points behind gold. Are you saying no one will do it again?

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

(The reason it didn't count was because their AI used too much time compared to the actual length of an IMO.)

@Bayesian Oh, clever. I do think there will be reasoning models which do get bronze or silver, even if they aren't reported on. Like people will just run o3 on the problems and report how it does; those might be sufficient to resolve.

@AdamK Plausible yeah.

@Forrest Did an AI get bronze or silver on any International Math Olympiad by end of 2025?

This is based on another market, which is based on a bet between Christiano and Yudkowsky, so if either of them mention an opinion on what should count, I'll probably defer to it.

As far as I'm aware, there are two issues which might be considered to disqualify the recent attempt: the use of manual translations to Lean, and the fact that it exceeded the time limit by roughly a factor of 15.

It is my current opinion that the 'translations' issue does not disqualify the attempt for the purposes of this market, but that the 'time limit' issue does, and thus that the criteria for YES have not yet been met.

However, I have not looked into the topic in depth yet, and cannot promise that I won't change my mind as a result of more research (nor will I promise to do said research in a timely manner - sorry)

Would be a good idea to have all of that in the description, seeing as this question as of today resolves YES. Thank you.

If there's been news today specifically, what I said above may be out of date.

I feel that having this in the comments is probably good enough, but will admit that if I were a better market creator I'd've given an opinion sooner.

there's not been news today, the official is just doing word gymnastics

I really don't think this qualifies. The "translations" to Lean do some pretty substantial work on behalf of the model. For example, in the theorem for problem 6, the Lean translation that the model is asked to prove includes an answer that was not given in the original IMO problem.

theorem imo_2024_p6 (IsAquaesulian : (ℚ → ℚ) → Prop) (IsAquaesulian_def : ∀ f, IsAquaesulian f ↔ ∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) : IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧ {(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2

The model is supposed to prove that "there exists an integer c such that for any aquaesulian function f there are at most c different rational numbers of the form f(r)+f(−r) for some rational number r, and find the smallest possible value of c".

The original IMO problem does not include that the smallest possible value of c is 2, but the theorem that AlphaProof was given to solve has the number 2 right there in the theorem statement. Part of the problem is to figure out what 2 is.

Link: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Thanks for pointing this out. I'm surprised that that I haven't seen anyone else say this. I agree with you that the question should not be resolved YES (yet).

They said they bruteforced the answer for the algebric questions, and then let the model prove it. So this does count. It's just multiple different components.

C.f. Gowers comment here, my understanding is that the formalizer network arrived at this additional information, and it was not provided by humans? https://x.com/wtgowers/status/1816840103349662114

This makes no sense to me. It basically works because the answers are guessable? Still highly skeptical. At the very least this limitation seems to preclude anything that doesn’t involve unconscionably vast compute resources, and solving any problem that does not have a cutesy toy answer that can be naively guessed (All even numbers/c=2, etc.). Certainly this should make others substantially more skeptical that this performance wasn’t just a fluke of the competition having so many answers of this type.

AFAICT It makes many guesses and disproves some proves others. It's a mixture of deduction and abduction, some version of this is done by people as well.

Actually I guess it was auto formalization at train time and human formalization at test time?

Seems like a rather critical detail.

The autoformalization step seems largely trivial. I’m guessing it has a small chance to be slightly off, and would disqualify the whole question. Since the IMO is a once per year attempt, they likely just didn’t want to take any chances.

Does it count if manual translation to formal language is required (as with DeepMind's recent result)? I would think it doesn't count...

Where does it say the translation of the IMO problems was manual? I see they mention a specially trained language model that translates English problems to formal statements, I assumed this was used for the IMO problems as well.

Where does it say the translation of the IMO problems was manual?

It says so in the blog post announcement. ctrl+f for "manual"

Does it count if manual translation to formal language is required

One of the people who formulated the bet in the linked market have said that this is fine.

how can anyone say llms are "really" intelligent when it takes them 3 days to get a silver medal performance on the IMO? it's obvious this will never be possible to be done under the 4.5 hours time limit of the competition

edit: /s (I thought it was obvious)

This wasn't solved by an LLM. And given computing advances, I see no reason to believe it is "never possible" to get under 4.5 hours.

94% seems about reasonable given that they have a year to make improvements and rent out more compute capacity if they want.

Pretty sure colorednoise is trolling.

I think it was solved by an algorithm using an LLM, the post says it used a "pretrained language model"

Not sure that he's trolling - seems more like seething.