"AI achieves silver-medal standard solving International Mathematical Olympiad problems"

[Edit: this comment is probably retracted, although I'm still confused; see discussion below.]

I'd like clarification from Paul and Eliezer on how the bet would resolve, if it were about whether an AI could get IMO silver by 2024.

Besides not fitting in the time constraints (which I think is kind of a cop-out because the process seems pretty parallelizable), I think the main reason that such a bet would resolve no is that problems 1, 2, and 6 had the form "find the right answer and prove it right", whereas the DeepMind AI was given the right answer and merely had to prove it right. Often, finding the right answer is a decent part of the challenge of solving an Olympiad problem. Quoting more extensively from Manifold commenter Balasar:

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

Early 2023 I bet $500 on AI winning the IMO gold medal by 2026 [LW · GW]. This was a 1:1 bet against Michael Vassar, meaning I attributed >50% to this. It now seems very likely that I'm going to win.

To me, this was to be expected as a straightforward application of AlphaZero-like self-play amplification and destillation. The missing piece was the analogous policy network, which was a convolutional neural network for the AlphaZero board games. Once it became quite clear that existing LLMs were capable of being smart enough to generate good heuristics to this (with enough data), it seemed quite obvious to me that self-play guided by an LLM-policy heuristic would work. 

Namely translating, and somehow expanding, one million human written proofs into 100 million formal Lean proofs.

We obviously should wait for the paper and more details, but I am certain this is incorrect. Both your quote and diagram is clear that it is one million problems, not proofs.

I don't think this [sc. that AlphaProof uses an LLM to generate candidate next steps] is true, actually.

Hmm, maybe you're right. I thought I'd seen something that said it did that, but perhaps I hallucinated it. (What they've written isn't specific enough to make it clear that it doesn't do that either, at least to me. They say "AlphaProof generates solution candidates", but nothing about how it generates them. I get the impression that it's something at least kinda LLM-like, but could be wrong.)

These kinds of math olympiad problems are quite similar in nature. So current models have a very good sense of what a "pattern" is

I saw someone claiming the opposite:

IMO problems are specifically selected to be non-standard. For the previous 10 years, I served as the national coach of the USA International Math Olympiad team ( https://www.quantamagazine.org/po-shen-loh-led-the-u-s-math-team-back-to-first-place-20210216 ). During the IMO itself, the national coaches meet to select the problems that will appear on the exam paper. One of the most important tasks of that group is to avoid problems that have similarity to problems that have appeared anywhere before. During those meetings, national coaches would often dig up an old obscure math competition, on which a similar problem had appeared, and show it to the group, after which the proposed problem would be struck down.

So, this AI breakthrough is totally different from #GPT being able to do standardized tests through pattern-matching. It strikes at the heart of discovery. It's very common for students to hit a wall the first time they try IMO-style problems, because they are accustomed to learning from example, remembering, and executing similar steps.

They already claimed once to be at a 1200 Elo level in competitive programming on the Codeforces, but in real competition settings, it only reached a level of, as I remember correctly, around ~500 as people found the corresponding account they used for testing.

I'd be interested in reading more about this. Could you provide a link?

I'm not sure it is different than for humans, honestly. First, I should give a standard disclaimer that different students have different strengths and weaknesses in terms of mathematical problem-solving ability, as well as different aesthetic preferences for what types of problems they like to work on, so any overview like the one I am about to give is necessarily reductive and doesn't capture the full range of opinions on this matter.

As I recall from my own Math olympiad days (and, admittedly, it has been quite a while), Combinatorics problems were generally considered to be the most difficult/tricky/annoying for the majority of contestants. This was because, unlike the vast majority of other fields, Combinatorics problems required a certain set of intuitions [? · GW] that could be described as "combinatorial taste", and solving them required you to understand the particular problem in front of you deeply, on an S1 level. You generally had to "play around" with the set-up for a fair bit, developing a better and better picture of what's going on, before certain insights just clicked in your head and guided you on the path to a solution.^[1]

Geometry, by contrast, was much more straightforward.^[2] Not in the sense that the problems were necessarily easier from an "objective" standpoint,^[3] but because you had an essentially fixed set of techniques and configurations you needed to understand (and mostly memorize) that would solve the vast majority of problems. As Evan Chen has said:

Very roughly, there are three different ways I try to make progress on a geometry problem.

• (I) The standard synthetic techniques; angle chasing, cyclic quadrilaterals, homothety, radical axis / power of a point, etc. My own personal arsenal contains some weapons not known to many contestants as well, most notably inversion, harmonic bundles and quadrilaterals, and spiral similarity / Miquel points.For this part, it’s highly advantageous to be well-versed with “standard” configurations and tricks. To give an extreme example: to solve Iran TST 2009, Problem 9 one essentially needs only recognize two configurations: a lemma about the midpoint of an altitude (2002 G7) and another lemma about the line (USAJMO 2014/6). Not knowing either of these makes it more difficult to solve the problem synthetically in the time limit. As a reference, Yufei Zhao’s lemmas handout contains a fairly comprehensive list of these configurations.

You also often had the opportunity to turn a geometry problem into an algebra bash, through complex numbers, barycentric coordinates, Cartesian coordinates, trigonometry, etc. These were skills you developed naturally by practice, and in many cases, if you were an experienced and well-prepared contestant, whenever you were given a Geometry problem, you would be able to instantly remember related problems and ideas and figure out the rough plan of how you needed to go about solving the problem. This is completely the opposite of Combinatorics, where you did indeed sometimes have recurring patterns or broad themes,^[4] but you mostly had to take each (worthwhile, IMO-level) problem on its own terms, instead of falling back on previously-memorized ideas.^[5]

Rather interestingly, this phenomenon (the distinction between the aesthetic of Combinatorics being centered on "deeply understanding and solving one problem" and the rest of the fields as "applying general techniques that expand the understanding of the entirety of Geometry, Algebra, etc.") was also noted at the research level by Timothy Gowers in his excellent essay on "The Two Cultures of Mathematics."^[6]

So, from this perspective, I suppose it would make a lot of sense for a rather narrow [LW(p) · GW(p)] AI system to be better at areas of olympiad Math that are more easily "systematizable" (such as Algebra and Geometry) and worse at the areas that seem to require a sort of deep understanding and problem-solving (like Combinatorics) that could plausibly get it closer to general intelligence.

1. ^{^}

   I think the standard example to illustrate this is problem 2 of the 2011 IMO (nicknamed the "windmill problem"), which had an average score of 1.5/7, which was roughly half of what the organizers generally aim for (meaning ~ 3/7, as in 2012), mostly because they underestimated how difficult it would be for the contestants to understand the (combinatorial) set-up properly given the time constraints.

2. ^{^}

   And so was Algebra, but to a lesser extent (although contestants working on inequalities, for example, also benefitted from a boatload of books filled to the brim with dozens of techniques and proof methods specifically geared for this).

3. ^{^}

   I'm not sure how such a thing could even be defined, anyway.

4. ^{^}

   If there actually was no structure to Combinatorics problems, then human minds would not be able to predictably perform better at solving them over time as they practiced more and more, which is false.

5. ^{^}

   To be fair, I have heard through the grapevine that this is getting less and less true as the years pass, because trainers are getting better and better at identifying and compiling books/documents, etc., for training specific combinatorial problem-solving techniques.

6. ^{^}

   Of course, there is a lot of nuance here that I am not getting into, and you shouldn't come away with the impression that Combinatorics is all just one-time tricks and the rest of math is just memorizing proofs that worked on previous problems. Reality is far more complex and multi-dimensional than that; there are parts of Combinatorics that work on the basis of deep theories (such as when using generating functions or the probabilistic method or when making connections with Statistical Mechanics, etc.), and also non-Combinatorial results that seem to have arisen from an almost purely individualized assessment of the problem (David Corfield mentions arithmetic progressions among primes as an example).

I searched for it and found none. The twitter conversation also seems to imply that there has not been a paper / technical report out yet.

No, but these tweets describe the basic concept: extension of AlphaZero to train on theorems in Lean automatically converted from natural-language proofs.

I'm guessing many people assumed an IMO solver would be AGI. However this is actually a narrow math solver. But it's probably useful on the road to AGI nonetheless.

People generally expected math AI to progress pretty fast already. I was angry about machine-assisted math being a neglected area before this and my anger levels aren't substantially increased by the news.

The news is not very old yet. Lots of potential for people to start freaking out.

Answer: it was not given the solution. https://x.com/wtgowers/status/1816839783034843630?s=46&t=UlLg1ou4o7odVYEppVUWoQ