The last IMO problem AI could not solve

Summary
Presented by Grant Sanderson (3Blue1Brown), this video explores Problem 6 from the 2025 International Mathematical Olympiad (IMO) in Australia, framed as the final contest problem of that year that frontier AI systems initially failed to solve. Sanderson delivers a complete derivation of both the optimal construction and its lower-bound proof using a geometric edge-matching argument, the Erdős–Szekeres theorem, and the AM-GM inequality. He concludes by analyzing why current AI reasoning models struggle with problems requiring exploratory patience and reflects on why human understanding—rather than raw proof generation—remains the central objective of mathematics.

---

What is shown

• [00:00] – [02:50]: Timeline of AI performance on IMO exams, showing AlphaProof’s 2024 performance (4/6 problems formalised in Lean), followed by 2025 models from DeepMind, OpenAI, Harmonic, and ByteDance solving 5/6 problems, with Problem 6 standing out as the sole unsolved question (solved by only 6 human competitors).
• [02:53] – [06:45]: Statement of Problem 6 on a $2025 \times 2025$ grid (where each row and column contains exactly one uncovered unit square) and simpler test grids ($10 \times 10$) demonstrating basic non-optimal configurations.
• [07:12] – [10:20]: Introduction of a motivating 3D cube-cutting brain teaser (slicing a $3 \times 3 \times 3$ cube into 27 unit cubes) to illustrate how lower-bound proofs rely on tracking invariant surfaces/edges rather than search algorithms.
• [10:22] – [18:50]: Discovery of the optimal windmill tile configuration using square tiles of size $k \times k$ tiled across a $k^2 \times k^2$ grid, establishing the candidate formula $(k-1)^2 + 4(k-1) = k^2 + 2k - 3$.
• [18:51] – [34:07]: Formulation of the rigorous lower-bound proof by mapping uncovered squares to highlighted directional boundary edges across four partitioned regions (top, bottom, left, right).
• [34:08] – [40:40]: Reformulation of the boundary paths into permutations of sequence indices, connecting the problem to longest increasing subsequences (LIS) and longest decreasing subsequences (LDS).
• [40:41] – [45:55]: Proof of $\text{LIS} \cdot \text{LDS} \ge N$ via the Erdős–Szekeres Theorem and application of the AM-GM inequality to prove $\text{LIS} + \text{LDS} \ge 2k$, calculating the exact minimum tile count of $2112$ for $k=45$.
• [45:56] – [51:55]: Discussion on AI progress in mathematics, citing researchers such as Thang Luong, Terence Tao, and Timothy Gowers on why human "motivated explanations" and holistic comprehension differ fundamentally from machine-generated verification.

---

Claims & numbers

• The presenter states that out of over 600 participants at the 2025 IMO on Australia's Sunshine Coast, less than 1% (exactly 6 students) earned full marks on Problem 6 [00:20].
• The presenter notes that Google DeepMind's AlphaProof solved 4 of 6 problems at the 2024 IMO using Lean autoformalization [01:45].
• The presenter states that in 2025, systems from DeepMind, OpenAI, Harmonic, and ByteDance solved all IMO problems except Problem 6 [02:10].
• For a general $k^2 \times k^2$ grid with one gap per row and column, the presenter proves the minimum number of rectangular tiles required is $k^2 + 2k - 3$ [17:52].
• For the specific 2025 contest problem ($2025 = 45^2$, so $k = 45$), the presenter calculates the exact minimum tile count as $45^2 + 2(45) - 3 = 2112$ tiles [45:35].
• The presenter cites the Erdős–Szekeres theorem to show that for any permutation of length $N$, the product $\text{LIS} \cdot \text{LDS} \ge N$, which implies via AM-GM that $(\text{LIS} + \text{LDS})/2 \ge \sqrt{N}$ [38:00–38:50].

---

Notable quotes

• [32:21]: (Quoting DeepMind research director Thang Luong): "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."
• [47:30]: "To me, knowing a proof is actually only one very small part of what it feels like to deeply understand a given piece of math."
• [51:20]: (Quoting IMO solver Aviv Tavor): "Rather, 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."

---

Assessment
This is a polished educational exposition and mathematical analysis video featuring 3Blue1Brown's custom programmatic animations (Manim). The visual proofs, combinatorial arguments, and timeline graphics are authentic pedagogical demonstrations rather than product demonstrations or promotional material.

Described by gemini-3.8-flash on 2026-10-07 from the video's audio and frames.