Twelve Puzzles, Each With a Proof (and Why That Wasn't Enough)
Breakout's difficulty was tuned statistically: a bot played ten thousand games and the clear rates said whether the levels were fair. That works for an arcade game, where difficulty is a distribution. It does not work for a puzzle game. A Sokoban level is not 15 percent solvable. It is solvable or it is broken, and if it is broken, the player you fooled into trying it will not come back.
So game five changes the question again. The first four posts asked whether the AI's code was correct and whether its tuning was fair. This one asks whether its content can be trusted, and answers with the strongest tool there is: a proof. Every level in the game below ships with a machine-checked certificate that it can be solved, plus the minimum number of pushes it takes. The HUD shows you that minimum while you play.
This post also has a second act it did not plan on, in which those proofs turn out to be necessary and nowhere near sufficient. Play first; the build below is the current, much meaner one.
arrows / WASD or swipe · Z undoes · R restarts · the title screen is the solver playing its own solution
The solver
Sokoban is a classic search problem, which is exactly why it fits this series: correctness you can enumerate. The solver Claude wrote is about eighty lines of breadth-first search with two ideas that matter.
First, it searches over pushes, not steps. Walking does not change a puzzle's state in any way that matters, so the player's position is collapsed into "which region can they reach," normalized to one representative cell. What is left is a graph where a state is the set of box positions plus a region, and an edge is a single push. The branching factor drops from four walk directions to only the pushes that are actually possible.
Second, it prunes stillborn states. A box pushed into a bare corner is never coming out, so any state containing one is skipped without expansion. With those two tricks, hard levels prove out in under a second, and a level with no solution exhausts its entire state space and comes back with the other kind of certainty: provably impossible.
That second kind turned out to be the important one.
A third of the first levels were broken
Claude was the level designer too, and it worked the way a human designer drafts: sketching wall shapes that felt like puzzles, placing boxes and goals, trusting its read of the geometry. Twelve levels came out of that. Then it ran make solve on its own work.
Four of the twelve came back provably unsolvable. A 33 percent defect rate, from the same session that wrote the working solver, and the rejects were not the ambitious ones. Two were levels the model was confident enough about that, without the gate, they would have shipped.
The traps were geometric and invisible to a read-through. The best one: a map with two wall stubs that split it into halves, connected through a single doorway cell. The intended solution parked a box on that doorway's far side, which worked fine, except the parked box then sealed the only route to the position needed for the final push. Every playthrough would have ended one move from victory, staring at a box that could never turn the corner. Claude initially disputed its own solver's verdict, re-traced the geometry step by step, and conceded: the level it designed and believed in was impossible.
The fix loop was mechanical: adjust the layout, rerun the gate, read the verdict. The gate exits nonzero if any level lacks a proof, so an impossible puzzle cannot ship without deliberately breaking the build. Twelve levels, twelve proofs, and the solver even set the level order, because Claude's hand-ordering had a six-push level in slot four and a ten-push level ahead of an eight. Confidence was high. The original twelve are preserved here exactly as they shipped:
the original hand-authored twelve, kept as the baseline · arrows / WASD or swipe · Z undoes
Then a human played them
The first person to play the set beat all twelve in one sitting. His review was two words: pretty easy.
He was right, and the reason is worth being honest about. The proof gate answers exactly one question, can this level be solved, and after it rejected four drafts, the redesigns drifted toward safety: wider rooms, more escape routes, boxes that could be handled one at a time. Every fix that made a level provable also made it tamer. The gate guaranteed correctness. Nothing in the pipeline measured whether a level was worth solving.
The difficulty ordering was also built on the wrong number. Ranking by minimum pushes sounds reasonable and is not: the set's "hardest" level needed 21 pushes but only 3,928 search states to crack, a long hallway pretending to be a puzzle, while an 11-push level made the solver sweat through 14,809 states. The truth was sitting in the column nobody used.
So the solver got a new job description: stop gatekeeping, start prospecting.
Mining for hard puzzles
Hand-designing harder levels was the obvious move and the wrong one; hand design had now failed at solvability and difficulty both. The replacement is generation, using Sokoban's classic trick: build levels backwards. Start from the solved state, boxes on their goals, and PULL them away with random walks. A pull is the exact inverse of a push, so every level generated this way is solvable by construction. The proofs become free, and the solver's real work moves to scoring: of thousands of guaranteed-solvable levels, which are hard?
The miner scores each candidate on signals from the solver's own optimal solution: states explored (search effort), box switches (how often the solution alternates between boxes, the interdependence the hand-made set lacked), and goal regressions (pushes that move a box away from its nearest goal, the counterintuitive moves). First run: 600 candidates, 137 survivors, five minutes of compute. The top scorers needed up to 45,297 states against the hand-made peak of 14,809. They shipped.
The same reviewer played the top-scored one and beat it. Easy, again.
That is the most useful data point in this whole post. States explored measures how hard a level is for a breadth-first search, which explores blindly. Humans do not explore blindly, they pattern-match, and a smallish open room with four boxes is a toy for a pattern-matcher no matter how much a blind search sweats over it. The metric was not wrong. It was measuring the wrong player.
The fix was not the metric but the ore body: the generator's rooms were too small and too open. Round two generates bigger boards, up to 13 wide, with denser walls, five-box configurations, pull-shuffles up to 200 moves deep, and a keep bar an order of magnitude higher. That made candidates roughly eight times more expensive to prove: the second run processed 124 candidates in 16 minutes and kept nine. The survivors are a different species, tight warrens where every wrong push matters, topping out at a level whose optimal solution took 78,859 states to find.
The reviewer's report card
The verdict on round two came back mixed, and the mixed part is where it gets good. Three of the mined levels finally made him think, and the finale earned real praise: it had an ordering trap, a level that cannot be beaten unless the boxes move in the right sequence, which is exactly the interdependence the box-switch metric was hunting for. The machine landed a punch.
But he also filed three bug reports. Two levels had a box sitting on its goal from the start, one of them walled in so completely he could not even reach it. Another had a box one push away from its spot, a checkbox pretending to be a puzzle. An audit of the shipped set matched his report level for level: the reverse-play generator only required two boxes to be displaced from their goals, so up to half a level's boxes could spawn pre-solved. The solver never objected, because a box already on a goal satisfies it, and no metric measured whether every box earns its place. The player was the instrument that caught it.
Round three added his findings as filters: every box must start off its goal, and every box must need at least two pushes in the optimal solution. The rejection stats show how much silliness those two rules delete: of the next 2,000 candidates, 175 died at generation for pre-solved boxes and 20 more for lazy ones, and four survived everything. Three of them replaced the flawed levels. The ones he validated did not move.
The set that ships now
| # | level | boxes | min pushes | states explored |
|---|---|---|---|---|
| 1 | First Push | 1 | 1 | 2 |
| 2 | Side by Side | 2 | 2 | 12 |
| 3 | Around the Post | 1 | 3 | 10 |
| 4 | Corridor | 2 | 6 | 36 |
| 5 | Warehouse | 4 | 11 | 14,809 |
| 6 | Prospect | 4 | 12 | 26,633 |
| 7 | Claim | 4 | 13 | 72,077 |
| 8 | Seam | 5 | 12 | 24,894 |
| 9 | Vein | 4 | 14 | 31,581 |
| 10 | Lode | 4 | 17 | 68,440 |
| 11 | Assay | 4 | 15 | 44,961 |
| 12 | Bedrock | 4 | 13 | 78,859 |
| 13 | Motherlode | 4 | 14 | 53,592 |
Four gentle openers survive from the original set, Warehouse holds the middle as the best thing hand-design produced, and the back eight are mined, named for what they are. Note the push counts barely move while search effort quintuples: difficulty was never about length. Two quality-of-life changes came with the harder levels: a box pushed onto a provably dead square, the same corners the solver prunes, tints red, and level select arrived so nobody is trapped replaying a finale.
Two kinds of confidence
This series has now used the harness two very different ways. Breakout's tuning was statistical: thousands of noisy games, confidence as a percentage. Sokoban's gate is logical: exhaustive search, confidence as a yes or no. Most real software verification lives on exactly this spectrum, load tests on one end and type systems on the other, and the interesting judgment is knowing which end your problem belongs to.
But this game added a third lesson the spectrum does not cover: a proof of correctness is not a measure of quality, and a machine's difficulty metric is not a human's. The gate stopped broken levels. The miner found levels that resist a blind search. Whether they resist a person, only a person can say, and after three rounds the scorecard reads like a negotiation: the human won round one outright, split round two on points while filing the bug reports that built round three's filters, and round three now sits at the top of this page. Every level in it exists because a proof said it works, a metric said it fights, and a person said what neither could see.
The code was never the hard part. The hard part is building the instrument that tells you the truth about what you made, and then noticing when it is telling you the truth about the wrong thing.