The Arrangement You Can't Always Make

In 1958 a mathematician watched his small son line up coloured blocks and noticed a rule the blocks happened to obey. The rule is so simple a child found it. Whether you can obey it turns out to depend, exactly, on a number being even.

Here is the whole puzzle. Take two each of the numbers 1, 2, …, n — that's 2n tiles — and lay them in a row so that:

the two k's have exactly k tiles between them.

So the two 1's are 1 apart, the two 2's have two tiles between them, and so on. For n = 3 there is essentially one answer: 3 1 2 1 3 2. Try to find it below by hand — then try n = 4, and then n = 5.

If you spent any time on n = 5, you were wasting it — and so was everyone else who ever tried. There is no arrangement for n = 5. None for n = 6 either. Press Solve it on those and the machine, having checked every possibility, tells you so. The puzzle that a child stumbled into is, for half of all n, flatly impossible.

When can it be done?

Build the answer up and a pattern appears: solutions exist for n = 3, 4, 7, 8, 11, 12, … and nowhere else — exactly the n that are 0 or 3 more than a multiple of 4. Drag the slider and watch the green squares: every fourth pair lights, in twos.

That is not a coincidence you have to take on faith. It falls out of one line of arithmetic — the kind you can watch happen.

The one-line reason

Number every cell by its position, 1 to 2n. Those positions add up to a fixed total no matter how you fill the row: 1 + 2 + ⋯ + 2n = n(2n+1). Now add them a second way — number by number. The number k sits in two cells whose positions differ by its gap d (that's k+1 in Langford's puzzle). So the two cells holding k contribute x + (x+d) = 2x + d. Summed over every number:

The left side is 2 × (a whole number), so it is even. The right side therefore has to be even too — and whether it is depends only on the parity of one famous quantity: the triangular number T_n = 1+2+⋯+n. Langford needs T_n to be even. And triangular numbers are even in a steady drumbeat — even, odd, odd, even, even, odd, odd, even — flipping with period four:

T_n is even exactly when n ≡ 0 or 3 (mod 4) — and that is the whole rule. The impossibility you felt at n = 5 was never a failure of cleverness. The total simply could not be split evenly; no arrangement could exist to find.

The mirror cousin

Shift the rule by a single step — let the two k's have k−1 numbers between them instead of k (so the two 1's sit adjacent) — and you get a different, equally old puzzle: the Nickerson variant, which is exactly what combinatorialists call a Skolem sequence. Switch the board above to it and the green squares move: now solutions exist for n = 1, 4, 5, 8, 9, …, the n ≡ 0 or 1 (mod 4).

The same one-line argument proves it. The only thing that changed is the gap — k instead of k+1 — which slides the deciding triangular number by one index, from T_n to T_n−1. Two puzzles that look like siblings, possible on interleaving halves of the number line, separated by nothing more than an off-by-one. (The board, the map, and the proof above all follow whichever you've selected.)

Every count, recomputed and checked

How many solutions are there, exactly? The table is computed two ways: the recomputing… count for your current n is found live, in your browser, by trying every possibility — and every entry is cross-checked against the published catalogue values in the On-Line Encyclopedia of Integer Sequences (A014552 for Langford, A059106 for Nickerson). They agree.

Counts are up to reversal: a row and its left-right mirror count once. The numbers explode — by n = 16 there are over six billion Nickerson sequences — which is why the live count above is run only for small n; the larger rows are the catalogued values, and the two agree wherever both are computed.

What's proved here, and what's borrowed

The argument on this page is necessity: it explains every impossibility you can hit, and nothing more. It does not prove that a solution always does exist when the parity allows — that a row can really be filled for every n ≡ 0,3 (mod 4). That harder direction, the actual construction, was settled by R. O. Davies in 1959 for Langford pairings and traces to Thoralf Skolem in 1957 for the Skolem/Nickerson sequences. We state their result as a citation, not as something re-derived here.

Machine-checked: the kernel pins the necessity law

The count table above cross-checks the rule by enumeration. It agrees with OEIS wherever both are computed, and the residue statement holds as far as we ran it (n ≤ 4000). But a search, however far it goes, only ever settles finitely many n. The necessity argument (a pairing exists, so T_n is even, so n ≡ 0,3 (mod 4)) is short enough to take a stronger check. Hand it to the kernel of Lean 4, a proof checker that believes nothing it cannot derive from its own logic, and it certifies the implication for every n, with no search at all.

theorem langford_necessity (n : Nat) (T : List (Nat × Nat))
    (hVals : (T.map Prod.snd).Perm (List.range n))
    (hCover : (cover langGap T).Perm (List.range (2 * n))) :
    n % 4 = 0 ∨ n % 4 = 3

theorem nickerson_necessity (n : Nat) (T : List (Nat × Nat))
    (hVals : (T.map Prod.snd).Perm (List.range n))
    (hCover : (cover nickGap T).Perm (List.range (2 * n))) :
    n % 4 = 0 ∨ n % 4 = 1

What the kernel adds is not a bigger board (the browser reaches further); it is certainty without trust for the necessity claim, now for all n at once rather than up to a bound. It does not prove the sufficiency direction, that a pairing exists for every allowed n; that stays Davies' and Skolem's construction, cited above. Every load-bearing theorem carries the footprint [propext, Quot.sound], with no sorry, no Classical.choice, and no native_decide. The concrete order-3 witness that shows the theorem is not vacuous depends on no axioms at all. Full proof, zero imports, reproducible from a fresh checkout in about a minute: research/langford/lean/Langford.lean.

The from-scratch enumerator (cross-checking the counts against OEIS A014552 / A059106 and the residue rule to n ≤ 4000), the Lean kernel proof of necessity for all n, and the full notes live in the project's notebook at research/langford/. C. Dudley Langford first posed the puzzle in the Mathematical Gazette in 1958, after watching his son.

1. C. D. Langford, "Problem," Mathematical Gazette 42 (1958), 228.
2. R. O. Davies, "On Langford's problem (II)," Mathematical Gazette 43 (1959), 253–255 (existence for all n ≡ 0,3 mod 4).
3. Th. Skolem, "On certain distributions of integers in pairs with given differences," Math. Scand. 5 (1957), 57–68.
4. OEIS A014552 (Langford), A059106 (Nickerson / Skolem).