The last IMO problem AI could not solve, and its value is not in the answer
In 2025, fewer than 1% of IMO contestants got full marks on Problem 6, and every AI was stuck on it. What makes it hard is not computation — it is that you must first understand, first have taste, before you start writing. And that is exactly what reinforcement learning struggles most to train.
The argument · tap a timestamp to hear it
What AI is stuck on is not computation, it is patience
In 2025, more than 600 top contestants worldwide took the IMO, and fewer than 1% got full marks on Problem 6. By 2025, models from multiple institutions could answer all the other problems correctly, but were stuck on this one. DeepMind research director Thang Luong's explanation: the model has no patience — it will not spend time understanding the problem or developing a feel for it, and instead starts solving immediately. Karpathy adds a second reason: the model has no sense of what makes a problem or a strategy beautiful, and the solution to this problem depends precisely on aesthetic judgment.
Genius is really the residue of experience
Facing this problem, the most obvious construction is to put all the X's on the diagonal, cover the remaining area with horizontal tiles, and get 2(n-1) tiles. But this construction is too obvious to be the answer the IMO wants. Karpathy inserts a seemingly unrelated cube-cutting brainteaser here: a 3x3x3 cube cut into 27 small cubes, where you are allowed to rearrange the pieces after each cut — what is the minimum number of cuts? The answer is 6, because each of the 6 faces of the very center small cube needs its own separate cut. This proof idea — fix your attention on one face of the internal structure — is exactly the key to the tiling problem later.
The most efficient tiling makes every tile touch four X's
Highlight the four edges of every X, and each time you place a tile, turn off the edges it touches. In an inefficient tiling, a tile touches only 1 or even 0 X's; in an efficient tiling, every tile touches 4 X's. This suggests a conjecture: the optimal tiling should make as many tiles as possible touch 4 different X's. But looking further, an X cannot fall in the middle of a tile edge — that would create a conflict between the two tiles above and below on the left, because a column cannot contain two X's. An X must fall on a corner of tiles, with four tiles arranged like a pinwheel around it. With square tiles of side length k, you can tile a large grid of side length k². 2025 happens to be 45², and this coincidence makes the construction look extremely promising.
Highlighting only one direction leaves out the tiles on one side
Highlight the edges of all X's, 4k² in total; each tile touches at most 4, and subtracting the 4 boundary edges that do not need to be touched gives the lower bound k²-1. But the target lower bound is k²+2k-3, off by a term proportional to k. The problem is that only the right edges are highlighted: the correspondence obtained this way is tight on the right side of the diagram, but misses a large number of tiles concentrated on the left. Switching to any single direction is the same — the missed tiles always cluster on one side. Karpathy says mathematics rewards you for respecting symmetry and punishes you for not respecting it — choose an arbitrary direction, and the weakness shows up in the inequality.
Cut the grid into four regions, highlight each edge only once
The solution is to draw two paths: one going up-right along the X's, one going down-right, dividing the whole diagram into four regions. If an X is in the right region, highlight its right edge; if in the top region, highlight its top edge; left, right, top, bottom each govern one region. An X on a boundary highlights two edges. This both fills in the missing highlighted edges and guarantees that each tile touches at most one highlighted edge — because when a tile sits in the left region, the X above it cannot highlight its bottom edge, the X below it cannot highlight its top edge, and the X to its left cannot highlight its right edge. This diagram is the core of the entire proof.
The problem reduces to a pure permutation problem
Label each X with the row number it is in; since each row has exactly one X, these labels form a permutation of 1 to k². The up-right path corresponds to an increasing subsequence, the down-right path to a decreasing subsequence. Let LIS be the length of the longest increasing subsequence and LDS the length of the longest decreasing subsequence; the total number of highlighted edges is k² + LIS + LDS - 4 (or +1 when the two paths intersect, making it -3). To prove the target lower bound k²+2k-3, it suffices to prove LIS + LDS ≥ 2k, that is, that their average is at least k. At this point the grid has completely disappeared, and what remains is a pure fact about permutations.
The proof of the Erdős-Szekeres theorem is itself a gem
This pure permutation fact is the Erdős-Szekeres theorem: in any permutation, the product of the lengths of the longest increasing subsequence and the longest decreasing subsequence is at least the length n of the permutation. An IMO contestant could simply cite the theorem and finish, but Karpathy chooses to give the proof as well. The method is to label each position with a pair of numbers: the length of the longest increasing subsequence ending there, and the length of the longest decreasing subsequence ending there. Because the numbers in a permutation are all distinct, the two label pairs at any two positions must be different — if the later number is larger, the first label increases by at least one; if smaller, the second label increases by at least one. Plot these label pairs as coordinate points; the longest increasing subsequence is the width of the bounding box, the longest decreasing subsequence is the height, and width times height equals the number of grid points, which is the length of the permutation.
Beyond the proof there is another layer: making the proof feel obvious
Karpathy says knowing a proof is only a very small part of deeply understanding mathematics. When he and Nishad Dulkhar made this video, their first reaction on seeing the original proof was, "I know it's true, but how would anyone come up with this?" What they want to contribute is not a new proof but a narrative that lets the viewer, when they reach the proof, no longer feel it came out of nowhere. He gives this thing a name: motivated explanation. This relates directly to AI and math: if a machine can generate proofs but does not bring human understanding, then it is completely meaningless. And academia has long used "proof" as a proxy metric for progress, which exposes an urgent need — a new, independent way to measure whether a publication actually advances human understanding.
In their own words · checked verbatim
It also seems likely to be the last IMO problem to be solved. No problem that AI could not solve.
we didn't really have a way to teach the model to be patient. It didn't take the time to understand the problem, to get a feel for the problem, to not try to solve the problem.
Thang Luong3:06
what can look like genius is usually the residue of experience.
math rewards you when your respected symmetries, and what we're seeing right now is how it punishes you if you don't.
I just think that's really lovely, too beautiful not to share.
if you're able to generate proofs that don't necessarily come with human understanding, that kind of completely defeats the point.
the value of this question lies in the fact that it warmed my heart when I solved it, and it still warms my heart more than a year later; like a good book or a touching song the value here is human.
Figures
| 2025 IMO participants | more than 600 teenagers | 0:00 |
| Full-mark rate on IMO Problem 6 | fewer than 1% | 0:00 |
| Number of full marks on 2025 IMO Problem 6 | 6 | 23:32 |
| Problems AlphaProof solved in 2024 | 4 out of 6 | 1:00 |
| 2025 grid side length | 2025, i.e. 45² | 16:23 |
Glossary
- Lean
- A programming language in which mathematical proofs are written as programs and can be verified by machine.
- Erdős-Szekeres theorem
- In any permutation, the product of the lengths of the longest increasing subsequence and the longest decreasing subsequence is at least the length of the permutation.
- motivated explanation
- A term coined by Karpathy: a narrative that makes a proof feel almost obvious to the reader, rather than merely followable step by step.
- LIS / LDS
- The lengths of the longest increasing (decreasing) subsequence in a permutation.
How to listen
Engineers and researchers interested in the intersection of AI and math, and in the act of understanding itself; anyone who wants to see the boundaries of model capability clearly.
The full solution walkthrough from 06:11 to 45:06, unless you actually want to work through the problem yourself.