In 2025, over 600 teenagers from all around the world gathered in the sunshine coast of Australia to compete in the International Math Olympiad. This contest consists of six highly challenging problems. And problem number six was the hardest by far. Despite every participant there clearly being a worldclass problem solver among the best of their country, less than 1% of the students managed to get full marks on it. It also seems likely to be the last IMO problem that AI could not solve.
[00:01:01] And that sentence would have sounded ridiculous to most people familiar with contest math even as few as 5 years ago. To solve one of these problems means writing up a full rigorous proof requiring imagination and creativity, not rote computation. In 2021, the IMO seemed like a different ballgame entirely for AI. In 2023 on Dwarkesh Patel's podcast, Grant was asked whether an AI getting gold at the IMO would just be AGI. In 2024, Google DeepMind's AlphaProof answered four of six questions (with human translation into Lean). In 2025, multiple organizations' models answered every question except problem six. By 2026, simply prompting public reasoning models was enough to get all six correct.
[00:03:00] Grant asked Tang Luong, a Google DeepMind research director, why the models struggled. Luong said they couldn't teach the model to be patient — it didn't take time to understand the problem before trying to solve it. Grant adds that models also lack a sense for what makes a problem or strategy beautiful.
[00:04:01] The problem: a 2025×2025 grid of unit squares. Matilda places non-overlapping rectangular tiles on the grid, aligned to grid lines, such that each row has exactly one uncovered unit square (marked X) and each column has exactly one uncovered square. Find the minimum number of tiles.
[00:05:00] Building intuition with a 10×10 example: naive tilings use 21, then 17, then 16 tiles. The task requires proving the minimum rigorously, not just finding a good construction. A diagonal-X construction gives 2n-1 tiles for an n×n grid, but this is not optimal.
[00:07:01] Grant introduces an analogous "warm-up" puzzle: cutting a 3×3×3 cube into 27 unit cubes with the fewest planar slices, allowed to rearrange pieces between cuts. The answer is 6, proved via a 1:1 correspondence — every one of the 6 faces of the inner 1×1×1 cube needs its own dedicated slice, since one slice can free at most one face.
[00:10:01] Applying similar thinking to the tiling problem: each edge of an X touches at most one tile, and each tile can touch at most one X-edge per side (up to 4 total). Comparing two 10x10 tilings, the more efficient one has tiles touching 4 X's each, arranged in a "windmill" pattern with X's at tile corners.
[00:14:00] Hypothesizing square tiles (respecting symmetry, best area-to-perimeter ratio): building a diagonal windmill pattern of k×k squares tiling a k²×k² grid, using (k-1)² interior tiles plus 4(k-1) boundary tiles = k² + 2k - 3 total tiles. For k=45 (since 2025 = 45²), this gives the conjectured minimum.
[00:17:00] Note: Australia's Sunshine Coast Airport floor (where 2025 IMO contestants landed) uses this exact windmill tile pattern — a real-world hint toward the construction.
[00:18:01] Proving the lower bound is the hard part. A naive "highlight all 4 edges of each X" argument gives only k² - 1 tiles (too weak — misses the +2k-3 term). A single-direction argument (highlight only right edges) also gives k² - 1 and is asymmetric/inefficient.
[00:25:00] The key proof idea: draw two paths through the X's — one connecting an increasing subsequence (up-and-right) and one connecting a decreasing subsequence (down-and-right) of the permutation defined by X row/column positions. These paths divide the grid into four regions. Highlight an X's right edge if it's right of both paths, top edge if above both, etc. X's on the paths get two highlighted edges (or four if on both paths' intersection). Critically, no single tile can touch two highlighted edges under this scheme.
[00:30:02] Counting highlighted edges: k² - 4 (base, minus 4 boundary exceptions) + LIS (longest increasing subsequence length) + LDS (longest decreasing subsequence length), plus 1 if the paths intersect. This gives a lower bound on tile count of roughly k² + LIS + LDS - 3.
[00:34:01] Remaining task: prove (LIS + LDS)/2 ≥ k = √(size of permutation). This reduces to the Erdős–Szekeres theorem: for any permutation of size n, LIS × LDS ≥ n. Combined with AM-GM (arithmetic mean ≥ geometric mean), this yields LIS + LDS ≥ 2√n = 2k.
[00:39:00] Proof of Erdős–Szekeres: label each element with (longest increasing subsequence ending here, longest decreasing subsequence ending here). These label-pairs are all distinct (a nice injectivity argument), so plotting them as lattice points in a box of width LIS and height LDS shows LIS × LDS ≥ n.
[00:43:02] Summary: the optimal construction (k² + 2k - 3 tiles, k=45 for the 2025 case) is proven optimal via the two-path/four-region highlighted-edge argument combined with Erdős–Szekeres and AM-GM.
[00:46:01] Reflection: Grant made this video with Nishad Dalal not to find a new proof (it already existed, including on the "Dedekind Cuts" YouTube channel) but to construct what he calls a "motivated explanation" — a narrative making a non-obvious proof feel almost inevitable. He argues understanding-generating "motivated explanations" should get academic credit alongside proofs themselves, especially as AI increasingly generates correct proofs without accompanying human understanding.
[00:49:00] Speculation on why AI struggled with this specific problem: heavy reliance on visual/geometric intuition (harder to train than symbolic reasoning), and the need to "understand and get a feel for" the problem before attempting a solution — a structure that's intrinsically harder for reinforcement-learning training environments.
[00:51:01] Closing quote from a Patreon commenter's friend who solved the problem: the value of the question isn't deep mathematical understanding or research difficulty, but that "it warmed my heart when I solved it," comparing it to a good book or touching song — a humanist argument that this kind of value can exceed an average PhD thesis.