Erdős–Szekeres Proves the 2025 IMO Tiling Minimum

Grant Sanderson frames the 2025 IMO’s sixth problem around a distinction that determines what counts as a solution. Producing a numerical answer is not enough. The task is to exhibit a tiling that achieves the claimed minimum and then prove that no other arrangement can use fewer rectangles.

The board is a $2025imes2025$ grid. It must be covered by non-overlapping, grid-aligned rectangles, leaving exactly one uncovered unit square in every row and every column. Mark those uncovered squares with Xs. There are 2,025 of them, and no two lie in the same row or column.

For a general board of side length $n$, the most immediate construction puts the Xs on the main diagonal and fills each side with horizontal rectangles. It uses $n-1$ tiles on either side, hence $2(n-1)$ tiles altogether. That establishes feasibility, but not an especially compelling candidate for optimality.

The more revealing construction starts from the fact that 2025 is a square:

Let the board side length be $k^2$. The source’s construction arranges $(k-1{)}^2$ interior squares of side length $k$ in a shifted array. The gaps occur at their corners. Around each interior gap, four square tiles form a windmill: each tile contributes one corner, and the four neighboring tiles meet without overlapping. The pattern’s shifted rows and columns keep the Xs in distinct rows and distinct columns. Rectangular tiles then fill the outer boundary.

The on-screen construction is load-bearing because it makes clear why the gaps must occur at corners rather than in the middle of tile edges. A gap has four sides that must abut tiles, except where a side lies on the exterior boundary. A tile can touch as many as four gaps and therefore cover four such local obligations. But if a gap lands in the middle of a tile edge, two tiles fitted above and below it have aligned opposite edges. Since the gaps cannot share a column, both cannot gain a gap on that side. One loses a possible contact. At a corner, by contrast, four tiles can meet in a windmill without creating that conflict.

Sanderson treats square tiles as a productive hypothesis rather than a theorem forced by the problem. Squares respect the symmetry of the setup, and they offer an efficient way to cover area while preserving the corner pattern. Once that hypothesis is in place, the square side length $k$ and board size $k^2$ fit together naturally. The source also notes that competitors arriving at the Sunshine Coast airport for the 2025 IMO could see the same basic shifted tiling pattern on its floor.

The interior contains $(k-1{)}^2$ square tiles. Each of the four sides needs $k-1$ boundary tiles, so the construction uses

For the original grid, $k=45$, giving

This proves that 2,112 tiles suffice. The harder half is showing that every valid tiling requires at least that many.

The proof starts from the same local observation that motivated the construction: every side of an uncovered square that does not touch the board’s boundary must touch a tile.

There are $k^2$ gaps and therefore $4k^2$ gap-edges. Four of those edges can lie on the outer boundary and need no adjacent tile. Since one rectangle can touch at most four relevant gap-edges, a first count gives

The lower bound is valid but inadequate. The construction uses $k^2+2k-3$ tiles, not merely $k^2-1$. The discrepancy is not accidental: the boundary tiles in the construction often touch only two gaps. Counting only average four-edge efficiency cannot capture the cost imposed by the board’s perimeter.

A sharper version highlights just the right edge of each X. Every highlighted edge, except the one at the far-right boundary, touches a tile. And a tile cannot touch right edges of two gaps, because the two gaps would then occupy the same column. This produces the same bound, $k^2-1$, but as a one-to-one association rather than a four-to-one average.

Its weakness is now geometrically visible. Highlighting right edges accounts well for tiles near the right side of the board, while the missed tiles cluster on the left. Highlighting top edges instead leaves the missed tiles clustered below. The method fails not because the association is invalid, but because it arbitrarily privileges one direction.

The repair uses four directions, each in the region where it has the advantage. Draw two paths through Xs: one traveling up and right, the other down and right. Together they form a wobbly cross and divide the board into four regions. In the right region, highlight right edges; in the upper region, top edges; in the left, left edges; and in the lower region, bottom edges. Gaps on a boundary path receive two highlighted edges.

The source’s diagram of this assignment matters because the additional highlighted edges are the mechanism for obtaining a lower bound larger than the number of gaps. The rule still has to preserve one condition: no tile may touch two highlighted edges.

Consider a tile in the leftward region. A gap above it cannot contribute a bottom edge under the regional assignment; a gap below it cannot contribute a top edge; and a gap to its left cannot contribute a right edge, which is reserved for the rightward region. The only possible highlighted contact is the left edge of the gap to the tile’s right. Thus the tile meets at most one highlighted edge. Rotating the same exclusion argument handles the other three regions.

The paths are therefore not a visual embellishment. They supply directional constraints that make the edge-to-tile association injective. Every highlighted edge requires a distinct tile. The remaining question is how many edges the two paths let the proof highlight.

Read the Xs from left to right and label each by its row number. Because every row contains exactly one X, these labels are a permutation of

An up-and-right path visits labels in strictly increasing order: it is an increasing subsequence of that permutation. A down-and-right path is a decreasing subsequence. Let their lengths initially be $A$ and $B$.

The regional assignment gives at least one highlighted edge for almost every gap. Four boundary edges may need no tile, producing $k^2-4$ base edges. Each gap on the increasing path receives an additional highlighted edge, contributing $A$; each gap on the decreasing path contributes $B$. Thus:

There is one necessary adjustment. If the two paths meet at an X, that gap has all four of its edges highlighted. Counting the gap once, then once for its presence on each path, registers only three of those edges. One more must be added.

If the paths do not meet at a gap, they cross through a tile. That central tile meets no highlighted edge, so it is an additional tile outside the edge assignment and can likewise be added to the lower bound. In either case,

Choose the paths to be longest possible. Write their lengths as $mathrmLIS$ and $mathrmLDS$, for longest increasing and longest decreasing subsequence. The tiling problem has become a statement about every permutation of $k^2$ elements:

To reach the construction’s count, it is enough to prove

That is the conceptual turn in the proof. The paths arise from an attempt to fix an asymmetric geometric count; their lengths are then controlled by a general theorem about permutations.

The needed permutation fact is the Erdős–Szekeres theorem in the form

where $N$ is the permutation’s length. Here, $N=k^2$.

Sanderson motivates the product bound with a family of examples. The ordered permutation $1,2,ldots,N$ has subsequence lengths $(N,1)$. If all the evens appear in increasing order before all the odds, the longest increasing subsequence has length at least $N/2$ while the longest decreasing subsequence has length 2. Grouping the numbers in three increasing residue classes suggests a pair near $(N/3,3)$. These examples point toward a product of at least $N$.

The shifted-square gap construction realizes the balanced case when $N=k^2$: both the longest increasing and longest decreasing subsequences have length $k$, so their product is exactly $k^2$. The same square geometry that gives the upper bound also illustrates equality in the permutation inequality.

The proof labels each entry in a permutation with an ordered pair:

Every pair is distinct. Take an earlier entry labeled $(x,y)$ and a later one labeled $(x^{\prime },y^{\prime })$. If the later value is larger, any increasing subsequence ending at the earlier entry can be extended to the later one, so $x^{\prime }geqx+1$. If the later value is smaller, the corresponding decreasing subsequence extends, so $y^{\prime }geqy+1$. Since the entries of a permutation are distinct, one of those cases must hold. No two entries share a label.

The source visualizes these labels as lattice points. Their first coordinates are at most the global $mathrmLIS$; their second coordinates are at most the global $mathrmLDS$. Thus all $N$ distinct points lie in a rectangle with

available lattice positions. The rectangle must contain at least $N$ positions, proving the theorem.

The theorem supplies the sum bound through the arithmetic mean–geometric mean inequality:

Hence $mathrmLIS+mathrmLDSgeq2k$, and therefore

Because the shifted-square construction achieves exactly that count, it is optimal. On the $2025imes2025$ board, the minimum is 2,112 tiles.

Sanderson introduced the problem as what was likely the last IMO problem AI could not solve. In 2024, he says, Google DeepMind’s AlphaProof answered four of six IMO problems after humans translated the statements into Lean, a formal proof language. In 2025, systems using both Lean and end-to-end natural-language approaches solved every question except this one. By 2026, Sanderson says, publicly available reasoning models could solve all six with prompting.

He does not reduce the problem’s resistance to AI to a single explanation. Its solution depends substantially on visual and spatial intuition, which he suggests may be harder to train than symbolic reasoning. He also points to Thang Luong, a Google DeepMind research director involved with a system that attempted the 2025 test.

That patience describes the proof’s actual structure. A solver cannot usefully begin by writing a formal argument. They need first to see the gap-edges as the right units of accounting; then see why windmill corners are efficient; then notice what the one-direction count misses; then discover why paths through gaps can repair it. Only then does a theorem about increasing and decreasing subsequences become a natural tool rather than an arbitrary trick.

Sanderson’s cube-cutting detour illustrates the role of prior experience in that process. A $3imes3imes3$ cube cannot be cut into unit cubes with fewer than six planar cuts, even if pieces can be rearranged after each cut. The central unit cube has six faces, and each requires its own cut. The insight is not a clever cutting technique. It is selecting the central cube’s faces as the objects that force a lower bound.

That template directs attention toward gap-edges in the tiling problem. The completed proof is concise; locating its organizing idea is not. Sanderson’s claim is that this distinction matters increasingly as machines become capable of generating proofs.

Sanderson and Nishad Deulkar were not trying to establish a new result. Evan Chen’s solution notes existed, and Dedekind Cuts had covered the problem on YouTube. Their question was how to make the proof’s moves feel motivated rather than like “a complete bolt from out of the blue.”

Sanderson calls the missing layer a motivated explanation. It reconstructs the pressures that make a proof available to human thought: why one counts edges, why the first count fails, why regional directions answer that failure, and why monotone paths create an opening for Erdős–Szekeres. The proof remains hard—only six students received full marks—but its formal steps need not feel arbitrary by the time they arrive.

For Sanderson, this is more than an instructional preference. Knowing that a proof works, articulating it rigorously, and constructing a narrative that makes its choices intelligible are distinct forms of engagement. The last can deepen understanding for its creator as well as its audience.

He argues that mathematics has historically treated proofs and solved open problems as proxies for intellectual progress. Yet the value of a result is often not its bare statement or an immediate application. It lies in the surrounding conceptual machinery: patterns of reasoning, new objects, and ways of seeing that can travel into mathematics and engineering. If proof-generating systems produce correct arguments without producing corresponding human understanding, proof certificates alone become a less adequate measure of progress.

Sanderson’s institutional proposal follows from that concern. Academic credit is deeply organized around proofs and publications, he says, and the community should try to formalize what a motivated explanation is and give it comparable standing when it genuinely advances human understanding.

The problem’s final value is not presented as practical utility or a major research breakthrough. Sanderson closes with a supporter’s relayed comment from someone who solved it: the question warmed their heart when they solved it and still did more than a year later, like a good book or a touching song. The construction, the proof, and the explanation all matter because they make that experience available.