The Coloring Was Forced

Take a chessboard and cut away two opposite corners. That leaves 62 squares. Can you cover them exactly with 31 dominoes, each covering two neighboring squares?

You cannot, and the classic reason takes one sentence. Color the board as usual. Every domino covers one light and one dark square, but the two missing corners are the same color, so the board has 32 squares of one color and 30 of the other. No set of dominoes can cover unequal numbers of light and dark squares.

The puzzle is usually told as a lesson in insight: the answer is easy once you think of the colors, and the trick is thinking of them. It has also served, as a recent paper notes, "as a test of automated reasoning since McCarthy", whose 1964 memo was titled "A tough nut for proof procedures". The paper, Building What a Proof Needs, tells it differently:

The classical colouring argument, usually presented as a clever idea, is here the output of a computation.

Dominoes as a table

Start by writing the puzzle down without any cleverness. Make a table with one row for each of the 62 squares and one column for each place a domino could lie. There are 108 such places. A full board has 112, and each removed corner takes away the two placements that would have covered it. In each column, put a 1 in the rows of the two squares that domino covers and 0 everywhere else.

A tiling is a choice of columns that covers every row exactly once. Now relax the question. Instead of choosing each domino or not, allow any amount of each domino, including fractions and negative amounts, and ask whether some combination of columns adds up to exactly 1 in every row. A negative domino makes no physical sense, but allowing it turns the puzzle into ordinary algebra, where a clean theorem says exactly when there is no solution. And if even that loose version has no solution, there is certainly no tiling. (If it does have one, nothing follows either way.)

The theorem is Fredholm's alternative, more than a century old. It says the loose version has no solution exactly when there is a way to put a number on each square such that the two numbers under every domino placement add to zero, while the numbers on the whole board do not add to zero. It is easy to see why such numbers rule out a tiling. If dominoes covered every square exactly once, adding up the totals under all the dominoes would give the total of the whole board. Every domino's total is zero, so the board's total would have to be zero too. Such a weighting is a certificate: anyone can check it, and once checked it rules out every tiling.

The computer finds the colors

How do you find such a weighting? You solve a system of linear equations, one equation for each of the 108 placements, by exact elimination with fractions, the method taught in school. All zeros would satisfy every equation, of course, but elimination does not stop at one answer: it finds every solution at once. What goes in is only the table of which squares each domino covers. Nothing about colors goes in. In the paper's words, the elimination is done "with no colouring supplied".

What comes out is the coloring. Every solution turns out to be a multiple of one pattern, and that pattern puts +1 on every square of one color and −1 on every square of the other. Every domino covers one of each, so its two numbers cancel. The board has 30 squares worth +1 and 32 worth −1, so the total is −2, not zero. That is the classic argument, recovered by arithmetic.

And it is the only one

Here is the part that goes beyond a demonstration. The paper proves that every weighting with the cancelling property is a multiple of the coloring: up to scale, there is exactly one. The paper calls such a weighting a linear certificate, and this is the sense in which the coloring is the only one. It is not the only possible proof that the board cannot be tiled.

The reason is simple once seen. If the two squares of every domino must cancel, then knowing the weight of one square fixes the weight of each neighbor, as its negative. Every square of the mutilated board can be reached from any other by stepping from neighbor to neighbor, so one choice fixes everything, and the only pattern that survives is the alternating one.

The colouring argument is therefore not one clever choice among many: up to scale it is the only linear certificate there is, and exact elimination recovers it without being told about colours …

The uniqueness, and the facts it rests on, are checked in Lean, a proof assistant that accepts only valid steps of logic. The elimination itself is an exact computer calculation, which you trust as far as you trust the program that ran it, and the paper marks the difference.

The same coloring on an uncut board sums to zero, because both colors appear 32 times. There the weighting still cancels under every domino, but it gives no obstruction, and indeed the full board can be tiled. The coloring only bites because the cut removed two squares of one color.

Another board, many certificates

The uniqueness comes from the simple structure of dominoes on this board: every square can be reached from every other by stepping across dominoes, and neighbors always have opposite colors. Any board with those two properties has just one such weighting. Tiling puzzles in general do not. The paper's next example makes the contrast. Can a 10 × 10 board be covered by bricks one square wide and four long?

Color the square in row r and column c by the remainder of r + c after dividing by 4. Any brick, lying either way, covers four squares in a row or column, one of each color. The four colors occur 25, 26, 25 and 24 times. Put +1 on the first color and −1 on the second, and every brick sums to zero while the board sums to −1. So there is no tiling.

But this time the certificate is far from unique. Exact elimination finds nine independent weightings that every brick cancels, which can be mixed in any proportions, and it pulls a working certificate out of them again without being told about colors. (Lean checks a weaker statement, that there are at least two independent ones.) With so many certificates to choose from, finding one says nothing special about it. On the mutilated chessboard there is only one, so the famous one is the only one. Behind the brick example sits a classical theorem of de Bruijn: a box can be filled with bricks only if each side of the brick divides some side of the box. Here the brick's length of 4 divides neither side of the 10 × 10 board.

Loosening a problem also has a limit: the loose version can have a solution when the real one does not. The paper's example uses a stricter loosening, fractions allowed but no negative amounts. Take two separate triangles, three points joined in a ring, and ask for a perfect pairing: a set of edges that touches every point exactly once. Neither triangle has one, since a triangle has an odd number of points. Yet putting half an edge on each of the six edges covers every point exactly once. A fractional pairing exists and a real one does not. As the paper puts it, "Nonnegative feasibility does not decide integral feasibility here": a fractional answer does not settle whether a whole-number one exists. A different classical theorem, Tutte's, which gives an exact test for when a network can be paired up, settles it. Boards like the chessboard, where neighboring squares always have opposite colors, cannot fool you this way: there, the paper notes, citing a standard result, a fractional covering with no negative amounts always yields a real one.

Where the idea comes from

The paper is about how proofs are built. In the solved cases it examines, the proofs move a problem to an auxiliary setting where an already established theorem applies (the paper calls it a law), use it there, and bring the answer back. It calls such a setting a leverage layer. Here the problem moves from dominoes to linear equations, the law is Fredholm's alternative, and the answer comes back as the total of −2. The paper is part of the Six Birds research programme.

What it does not say

The chessboard mathematics is classical, and the paper says so. The coloring argument is folklore, Fredholm's alternative is more than a century old, and "These theorems are elementary, and they are not the contribution." The chessboard is a worked example, and the paper is explicit about what such examples can show: "Both experiments are reconstructions for teaching, not history." More broadly, "The demonstrations are not evidence of discovery power. They are worked examples written by an author who knows the answer."

The computation found the coloring once the problem had been written as a table and loosened to allow fractions. Loosening it that way was part of setting the problem up, and the paper's step-by-step record of the example lists it as a deliberate move, stated in advance. That is where the human judgment went, and it fits the puzzle's reputation as a hard case for automatic reasoning. What the result does show is that, once the problem is set up that way, the famous insight was not a lucky guess among many possible weightings. It was the only one, and a computation would have handed it over.

Drawn from Building What a Proof Needs: A Method for Constructing Leverage Layers (Tsiokos, 2026, version 1, doi:10.5281/zenodo.23097947). The counts, examples and quotations are from the paper, including its citations of McCarthy (1964), Fredholm (1903), de Bruijn (1969) and Tutte (1947); no new computation is claimed by this essay.