.png)
9 hours ago
2
With the 2025 International Math Olympiad underway, there's a lot of excitement and questions about how well AI will do. Will DeepMind beat their performance last year and get gold? Will frontier models be found overfit? Will formal or informal methods prevail?
I don't have any direct connection or inside scoop on the companies competing at the IMO, but I have participated both as a contestant and as a team leader for the IMO, been working in AI/ML, and have been building out AI tools to help with math research. So I thought it would be fun to lock in my bet before we hear the final results!
I'll update as results come in, and as we get the Day 2 problems.
Day 1 Question 1
Problem Statement
A line in the plane is called $sunny$ if it is not parallel to any of the $x$–axis, the $y$–axis, or the line $x+y=0$.
Let $n\ge3$ be a given integer. Determine all nonnegative integers $k$ such that there exist $n$ distinct lines in the plane satisfying both of the following: for all positive integers $a$ and $b$ with $a+b\le n+1$, the point $(a,b)$ lies on at least one of the lines; and exactly $k$ of the $n$ lines are sunny.
Resources
- Solution video
- AoPS thread (temporarily down)
- LLM Responses (None of the major LLMs get the right answer)
Analysis
This is a fairly challenging problem 1, and should be hard for both humans and AIs. The answer looks a bit strange and unintuitive, but ultimately just requires one major trick and some case work. I wouldn't be surprised if several people get docked partial marks for missing a case.
I expect it will be especially tricky for AI since it requires geometric intuition and is the kind of combinatorial problem that is tough to formalize. Given how many different ways there are to formalize a problem like this, I would look very carefully at the formal statement each team provided, since teams can cheat by picking an especially easy formulation.
Deepmind did not attempt combinatorics last year but since then autoformalization of combinatorics problems, and hence the potential for RL on it, has pushed ahead significantly.
This problem will be a great litmus test.
Day 2 Question 2
Problem Statement
Let $\Omega$ and $\Gamma$ be circles with centres $M$ and $N$, respectively, such that the radius of $\Omega$ is less than the radius of $\Gamma$. Suppose $\Omega$ and $\Gamma$ intersect at two distinct points $A$ and $B$. Line $MN$ intersects $\Omega$ at $C$ and $\Gamma$ at $D$, so that $C, M, N, D$ lie on $MN$ in that order. Let $P$ be the circumcentre of triangle $ACD$. Line $AP$ meets $\Omega$ again at $E\neq A$ and meets $\Gamma$ again at $F\neq A$. Let $H$ be the orthocentre of triangle $PMN$.
Prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of triangle $BEF$.
Resources
- Solution video
- AoPS thread (temporarily down)
- LLM Responses
Analysis
This is the kind of angle chasing solution that should be easy for AlphaGeometry and any model trained explicitly on geometry problem. I expect a purely informal system will not be able to solve it, but potentially a general formal system with access to a geometry library will, and that would be very exciting.
There's a lot going on in the problem and students could easily get bogged down keeping track of it all, especially with the competition pressure, but that's not a big challenge for computer systems.
Day 3 Question 3
Problem Statement
Let $\mathbb{N}$ denote the set of positive integers. A function $f\colon\mathbb{N}\to\mathbb{N}$ is said to be bonza if $$f(a)\quad\text{divides}\quad b^a-f(b)^{f(a)}$$ for all positive integers $a$ and $b$.
Determine the smallest real constant $c$ such that $f(n)\leqslant cn$ for all bonza functions $f$ and all positive integers $n$.
Resources
- Solution video
- AoPS thread (temporarily down)
- LLM Responses
Analysis
I'm glad I was working on this problem without the pressure of being in a competition. It can be easy to make mistakes when wrapping up the cases, or get stuck in a wrong direction, especially with the psychological impact of this being a problem 3.
Questions where you have to find something are harder for AI systems than questions where you have to prove something. In this case the best $c$ value cannot be readily guessed, so some systems could get bogged down with this. That said, Grok 3 Mini comes up with the right answer and a handwavy explanation. Does it have web access to these solutions?
However the actual solution is not too bad, simply applying standard approaches for functional equation and number theory problems, with steady indicators of progress and being on teh right track, so I would expect most AIs would be able to brute force this out (assuming they don't get stuck on guessing the right answer)
