The Verification Venue · Pattern · machine-checked

The Mutilated Chessboard

Snip two opposite corners off a chessboard. Sixty-two squares remain — an even number, room for exactly thirty-one dominoes. Lay them down and you will never cover the board. Not because you weren't clever enough: because of colour. Try it below, watch it strand two squares every time, then turn the colours on and see why — a one-line argument that beats a search of nearly thirteen million tilings, and is checked here by a machine.

Covered
0 / 62
Light left
30
Dark left
32
Holes
2

What just happened

The puzzle looks fair. Sixty-two squares, an even number; thirty-one dominoes, each covering two squares; 62 = 2 × 31. Nothing about the count forbids it. And there are vast numbers of ways to lay dominoes — the intact 8×8 board can be tiled in 12,988,816 different ways. Surely one of them dodges the two gaps?

None does, and the reason ignores the search entirely. Turn on Show the colours and look at the two squares you removed: they are the same colour. That is the whole story. Colour the board like a chessboard. Every domino — horizontal or vertical, anywhere — sits on two adjacent squares, and adjacent squares always have opposite colours. So every domino covers exactly one light square and one dark square. A full tiling of 31 dominoes would therefore cover exactly 31 light and 31 dark. But the two opposite corners are both light, so cutting them off leaves 30 light and 32 dark. Thirty cannot pair with thirty-two. No tiling exists — and no amount of cleverness will change a count.

This is a parity invariant: a quantity (here, light − dark) that every legal move leaves unchanged, but the goal demands you change. Place a domino and the count of uncovered light and uncovered dark each drop by one — the difference never moves off +2. You can shuffle dominoes forever; you can never make 30 equal 32. It is the same reason you can't make change for a pound with an equal number of two coins when you're holding thirty of one and thirty-two of the other.

So when can you do it?

Switch to Pick the two holes and remove a different pair of squares, then press Auto-solve. You'll find the dividing line is purely colour: remove two squares of opposite colour and the rest always tiles; remove two of the same colour and it never does — no matter where on the board they sit. The colouring argument forbids the same-colour case. The opposite-colour case is a real theorem too (Gomory, 1973): thread a single closed loop through all 64 squares visiting each once; removing one light and one dark square cuts the loop into two arcs of even length, and each arc tiles by taking alternate steps. Either way, the board itself tells you the answer the instant you press solve — it runs an exact matching, not a guess.

Show the check

Nothing here is asserted. The board decides tileability by exact bipartite matching (a region of 2k squares tiles iff its maximum matching has k dominoes) — the same code runs offline in research/the-mutilated-chessboard/verify.mjs, which checks all 2016 ways of removing two squares and confirms the region tiles if and only if the two removed squares differ in colour — 2016/2016, no exceptions — and recomputes the 12,988,816 tilings of the intact board (Kasteleyn). And the impossibility direction is machine-checked in Lean: research/the-mutilated-chessboard/lean/MutilatedChessboard.lean proves that no list of dominoes can cover exactly the mutilated board — for every board, by the colour invariant, with zero imports and axiom footprint [propext, Quot.sound]. A search can only check finitely many boards; the proof settles all of them at once.

Why a one-liner beats the search

This is the quiet power of an invariant. To rule out a tiling by brute force you would have to inspect an astronomical number of arrangements and find every one wanting — the intact board alone has 12,988,816; the mutilated board has its own forest of partial layouts to exhaust. The colouring does it in a sentence, and does more: it tells you exactly which deletions are impossible (any two of one colour) and which are fine (one of each), for boards of any size, without drawing a single domino. The same shape of argument proves you can't always solve the 15-puzzle, can't tile other deficient boards, can't reach certain states of a Rubik's cube. Find the invariant and the search evaporates.

What is, and isn't, claimed