Loyd's 14–15 swap cannot be slid back to solved with the gap home. The reason is one bit of arithmetic that no move you make can ever flip.
research/fifteen-puzzle/verify.mjs (36/36), computed live from the board being drawn (re-enacted, not quoted); the music is a declared sonification of the same BFS and parity. Build after provisioning Node.js, Playwright with Chromium and its system libraries, and ffmpeg (set PLAYWRIGHT_BROWSERS_PATH if Chromium is outside /opt/pw-browsers): bash research/fifteen-puzzle/film/build.sh.
The film still carries the universal three-cycle claim. Both the film and poster still carry the old prize date, the unsupported St Louis label, and the claim about the prize's impossibility and Loyd's knowledge. See the Corrections note.
In January 1880 a small wooden box of fifteen numbered tiles set the United States, and then Europe, briefly out of their minds. You slid the tiles one at a time through the single empty square, trying to put them in order. Years later, in the Illustrated American on 4 January 1896, the puzzle-maker Sam Loyd published a challenge with 14 and 15 swapped, offering a $1000 reward to be divided among solvers. Slocum notes that the published wording left the gap's final position unspecified; the impossible task shown here requires it back in its corner.
Loyd later said the prize was never claimed. With every tile and the gap required home, the task is impossible. Worse than that: the impossibility isn't a quirk of his one setup. Of all the ways you could ever arrange these tiles, exactly half can never be reached by sliding, no matter how long you push them around. Loyd's box simply started in the wrong half. Here it is. Try to fix it.
Stop thinking about tiles and think about the gap. Every legal move does exactly one thing: the gap trades places with a tile next to it. In the language of permutations, that is a single transposition — two items exchanged, nothing else. The whole puzzle is just a long chain of transpositions applied to the starting order.
And transpositions have a property they cannot shake. Mathematicians attach a sign to every arrangement: +1 if it takes an even number of swaps to reach from the solved order, −1 if odd. (This is well-defined — the count's parity never depends on how you swap.) Each move flips the sign, every time: even ⟷ odd. So the sign of the tile arrangement is a coin that turns over on every single move you make.
Starting with an odd arrangement and the gap home, you can never reach the solved board with the gap home: returning the gap to its corner takes an even number of moves, so the sign ends where it started. Loyd's swap is a single transposition away from solved: sign −1, odd. To undo it you'd need an odd number of moves, but any path that brings the gap home uses an even number. The parities can't be made to agree. That mismatch is the wall.
Here is the exact invariant, the thing every legal slide leaves untouched. Take the sign of the arrangement and combine it with where the gap is:
J = sign(arrangement) × (−1)(taxicab distance of the gap from home)
Why is J frozen? A slide flips the sign (one transposition) and moves the gap one step (changing its taxicab distance by exactly one, flipping that second factor too). Two flips multiply to no change. So whatever J was at the start, it stays — through one move or ten million. The solved board has J = +1. Therefore:
a board is solvable ⟺ J = +1
You can read this bit straight off any arrangement without sliding a single tile — and below, you can watch a live search confirm that the bit is never wrong. Set a board, and the oracle reads its J and gives a verdict instantly. Then press prove it by search: the program quietly builds the entire universe of boards you can reach from solved — all 181,440 of them — and checks whether yours is in it. The arithmetic and the brute-force search always agree.
The search isn't just a demo — it settles the claim independently of the parity argument. Run from the solved 3×3, it reaches 181,440 distinct boards and then stops, having found every move dead-ends back into the same set. That is exactly 9! / 2 — precisely half of the 362,880 arrangements three rows of tiles can take. The other half forms a second island the gap can never bridge to. (The full 15-puzzle is too vast to map this way — about 1013 boards — but the same parity bit cleaves it in two all the same: half reachable, half not.)
When the gap is back in its home corner, the reachable boards are exactly the arrangements with even sign, the mathematicians' alternating group, An, which is always precisely half of all permutations. One sharp consequence: you can never swap just two tiles and leave the rest. A two-tile swap is a single transposition, sign −1, odd, and locked out. (Brute force agrees: of the 20,160 reachable home boards, the number that differ from solved in exactly two tiles is zero.) The smallest real rearrangement you can make is a three-tile cycle: rotate three tiles around and leave everything else, because that takes two swaps, and two is even. An apparent two-tile swap need not hide a three-cycle: in Jaap Scherphuis's letter puzzle, two identical R tiles also swap, making two transpositions, an even permutation.
With the gap required home, the mathematical wall is absolute. The impossibility was proved in 1879 by William Woolsey Johnson and William E. Story in the American Journal of Mathematics. Johnson supplied the parity obstruction you've just been sliding around in; Story supplied the complementary solvability construction and its generalization. That wall had been described in print before Loyd's documented prize challenge.
For decades Loyd claimed he invented the puzzle. He did not. The historians Jerry Slocum and Dic Sonneveld traced the real origin to Noyes Palmer Chapman, a postmaster in Canastota, New York, around 1874; Loyd's authorship claim first appeared in 1891 and he repeated it until his death in 1911, a story that "fooled everyone for 115 years," as Slocum put it. The man who published the 1896 challenge had also taken credit for a puzzle he didn't make. The mathematics, at least, has never lied: half the arrangements are unreachable, the line between the halves is one unflippable bit, and you can check every word of it below.
The search on the 3×3 is airtight, but it is still a search: it visits 181,440 boards and stops. The real 15-puzzle has about 1013 arrangements, and a grid can be any size at all, and no search reaches the end of that. So the load-bearing claim, the parity bit J is preserved by every legal slide, on a board of every width and height, is handed instead to a proof assistant, which settles all sizes at once. research/fifteen-puzzle/lean/FifteenPuzzle.lean (Lean 4, zero imports, so the only trusted component is the kernel) proves it in two independent halves that meet at the end:
swap_flips). Writing the arrangement as a :: (M ++ b :: S) (the blank a, then the cells M between, then its neighbour b), transposing a and b changes the inversion count by an odd number. The entire content is that the two orderings' inversion counts sum to something odd: the mixed a-vs-M and b-vs-M terms pair up to exactly 2·|M|, and all that survives is the single a-vs-b comparison, which is odd because a ≠ b.cellSum_flip). The blank's row + column changes by exactly one on any legal step (right by a column, not off the row edge, or down by a row), so its parity flips too.Two flips cancel, so J is preserved (slide_preserves_J), constant across every board a sequence of slides can reach (reachable_preserves_J), and the board that swaps two tiles has the opposite J, so it is walled off forever (two_swap_unreachable), Loyd's 14–15 board being the named 4×4 case (loyd_unreachable). The Slide relation is a faithful model of a real slide (a horizontal move is M = [] with the gap off the edge, a vertical move is |M| = w−1, both directions allowed), and two worked examples prove it is genuinely inhabited, so none of this is vacuously true. Every theorem's axiom footprint is [propext, Quot.sound]: no sorry, no Classical.choice, no native_decide. What the kernel adds to the search is the one thing a search can't give: all the sizes, not the ones that fit in memory.
[propext, Quot.sound] in the five named theorem footprints when the toolchain is present.
Wm. W. Johnson & W. E. Story, "Notes on the '15' Puzzle", American Journal of Mathematics 2 (1879) 397–404 — the first proof of impossibility and the parity invariant.
R. M. Wilson, "Graph puzzles, homotopy, and the alternating group", J. Combinatorial Theory Ser. B 16 (1974) 86–96; the general theorem: on a non-separable graph, legal moves reach all or exactly half of the labelings, with polygons and one other graph excepted.
Jerry Slocum & Dic Sonneveld, The 15 Puzzle: How It Drove the World Crazy (Slocum Puzzle Foundation, 2006) — the documented history: Noyes Chapman's authorship (c. 1874), the 1880 craze, and the dismantling of Loyd's claims.
Historical summary cross-checked against David Richeson, "A picture of frustration: Sam Loyd's 15 puzzle" (2011) and Jaap Scherphuis, "The Fifteen / 14-15 puzzle" (jaapsch.net). The mathematics (the count 181,440, the invariant, the 3-cycle minimum, the 8-puzzle diameter of 31) is computed from scratch in the verifier — not taken from any source.
Corrected 2026-09-28 (found by a scan of the site's pages for verdicts printed whatever the page computed): the live check panel ticked every line, and the search result said "exactly 9!/2" and "the search agrees", without comparing anything. The claims were true, but the page did not check them. Now each tick and each "agrees" depends on the value the page computed, and the panel's 181,440 line points to the search button instead of ticking a count it has not run.
Corrected 2026-10-14: The plain summary dated Loyd's $1000 offer to 1880, and the opening placed it in that craze. Slocum dates the first published challenge to 4 January 1896. The 1896 wording left the gap's final position unspecified; the impossibility shown here requires it home. The film source also attached the prize to 1891; that year belongs to Loyd's inventorship claim. The film source's chronology is corrected, but the existing film and poster still carry the 1891 prize date and an unsupported St Louis label; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page credited Story with the parity reason. Johnson supplied the parity obstruction; Story supplied the complementary solvability construction and generalization; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said you could never get back to solved with the gap home. Two legal moves can return to solved; the obstruction applies to an odd starting arrangement with the gap home; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said every apparent two-piece grid swap hid a three-cycle. Scherphuis's letter puzzle instead swaps two visible letters and two identical R tiles, a double transposition. A three-cycle remains the smallest nontrivial rearrangement with the gap home. The page and film source are corrected; the film still carries the universal claim; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said the 3×3 search visits 362,880 boards. It reaches 181,440; 362,880 counts all arrangements, which the verifier enumerates separately; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page said the live Lean check enforced the [propext, Quot.sound] footprint. It rejected only sorryAx and Classical.choice, allowing an added axiom to pass. When Lean is available, it now requires reports for all five named theorems and rejects every axiom outside propext and Quot.sound; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page described Wilson's result as alternating-only on almost every puzzle graph. His theorem permits all or exactly half of the labelings on a non-separable graph, except polygons and one other graph; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page promised a film rebuild from a fresh checkout. The command also needs Playwright, Chromium and its system libraries; these are not supplied by the checkout. The build prerequisites are now stated. No film was rebuilt in this pass; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The nearby-layer note called both topics permutation parity and said Thue-Morse turns cancel the first mover's advantage exactly. Thue-Morse uses binary digit parity; the puzzle combines permutation parity with gap position. ABBA shares of 8, 4, 2, 1 total 9 and 6. Exact power-sum equality holds below degree m on the block 0 through 2^m - 1; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page introduced the first board as Loyd's impossible swap, but initialized it with a solvable shuffle. It now opens with 14 and 15 exchanged and J = −1; found by the assay line, 2026-10-14.
Corrected 2026-10-14: The page and film treated the prize challenge as impossible and inferred that Loyd knew it. Slocum describes the published 1896 problem as solvable: it did not specify the final gap position. The parity obstruction here applies to the goal with every tile and the gap home. The page and film source are corrected; the film and poster still carry the old claim; found by the assay line, 2026-10-14.
Claims record for this pass. The film and poster corrections remain open.
Written 2026-06-20. Claims re-read against their sources on 2026-10-14: 142 checked, 120 confirmed, 20 wrong, 0 unverifiable, 2 true when written and overtaken since (dated, not corrected). By the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex; fix-check repair by Codex.
This record covers the 20 queue-1014c triage items and the subsequent fix-check repair. The 120 CONFIRMED lines retain the checker's attributed source rereads at f5e5f84f34. Two previously confirmed historical inferences are now WRONG (R1 and R2) after comparison with Slocum's account of the published challenge. Counts are 120 CONFIRMED + 16 WRONG + 4 MINOR + 2 STALE = 142; the wrong field includes the four MINOR findings. X5, X17, X18, R1 and R2 remain open in the encoded film or poster despite corrected editable text. The claims gate will reject these placeholders until then.
This record is long (142 claim lines and 22 findings), so it is not part of the page until you open it. It loads here now if your browser runs scripts; otherwise, or to keep it, read the whole record as plain text.
The assay office: what a record is, and every layer re-read so far.