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 leave at least two squares uncovered, then turn the colours on and see why: a one-line argument that needs no search, and is checked here by a machine.

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. You cannot pair every one of thirty light squares with every one of thirty-two dark squares.

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, reported by Gardner in November 1962): 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.

Why a one-liner beats the search

This is the quiet power of an invariant. An exhaustive search can rule out a tiling: Knuth reports a completed search of the mutilated board. The colouring settles the impossibility in a sentence. For this 8×8 board, it forbids any two holes of one colour; Gomory's closed-loop construction supplies a tiling when one hole is of each colour. The same shape of invariant 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

• The 8×8 board has 32 light and 32 dark squares; the two opposite corners are the same colour, so the mutilated board is 30 vs 32. (verified)
• Every one of the 112 possible domino placements covers one light and one dark square. (verified, exhaustively)
• The mutilated board has no domino tiling — decided by exact matching, and proved for this 8×8 board with (0,0) and (7,7) removed in Lean. (machine-checked)
• Across all 2016 two-square removals, the rest tiles iff the two squares differ in colour. (verified, exhaustively)
• Not claimed: that matching is how a human should see it. The point is the opposite — the colour argument needs no search at all.