Everything a computer can do, this can do. Slower, but you can watch. Five machines, each one idea past the last; every step is said in words as it happens.
The lock opens only when every switch is on. Checking a setting walks along it once: 2 steps for one switch, 11 for ten, one more for each switch added. Finding the setting by trying them in order, checking each, more than doubles with every switch: 6 steps for one switch, 22,517 for ten.
The lock is simple on purpose, so you can see the answer before the machine does. What it shows is the gap: checking a proposed answer stays cheap while finding one grows out of reach. That gap is why checking someone else’s proof is feasible at all: the checker never has to find the proof, only follow it.
For a whole family of such puzzles, 3-SAT, the Exponential Time Hypothesis (Impagliazzo and Paturi, 1999) says no machine, however clever, can keep the work from multiplying by some fixed factor above one with each switch added. In October 2026 OpenAI and Anthropic each published a Lean proof meant to show that it is false. What I checked in those proofs.
10 switches: checking 11 steps, finding 22,517, which is 2.20 times the count for 9.
| switches | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 |
|---|---|---|---|---|---|---|---|---|---|---|
| checking | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 |
| finding | 6 | 21 | 60 | 155 | 378 | 889 | 2,040 | 4,599 | 10,230 | 22,517 |
Running a machine can show that it stops: you watch it stop. Running can never show that it does not, because at every step it might still stop at the next one. So a checker that only runs things needs a third answer besides yes and no. On this site that answer is REFUSED: not false, only not decided by this check.
The busy beaver question asks it at full strength: of all the machines with n states that stop on a blank tape, which runs longest? Answering it means settling every other machine of that size, including each one that never stops, and each of those needs an argument, not a run.
| states | the longest run that stops | how it is known | in your tab |
|---|---|---|---|
| 2 | 6 | Radó, 1962 source | |
| 3 | 21 | Lin and Radó, 1963 source | |
| 4 | 107 | Brady, 1983; formalized by the bbchallenge project in 2024 source | |
| 5 | 47,176,870 | the bbchallenge Collaboration, 2024, proved in the Coq proof assistant (now Rocq): 181,385,789 machines settled source | |
| 6 | Refused not known | unknown; the best lower bound, found by mxdys in June 2025, is more than 10↑↑10↑↑10↑↑8, and since Antihydra (June 2024) settling it means solving a problem like Collatz’s source | no champion to run |
Your tab runs each champion and confirms that it stops after exactly that many steps. That no other machine of its size runs longer is what the cited proofs establish; a run cannot.
Each claim names a machine and what it is given. Decide runs it in your tab with a budget of 1,000,000 steps: Certified when the run ends the way the claim says, Refuted when it ends the other way, Refused when the budget runs out first.
abba reads the same both ways.
abab reads the same both ways.
Some setting of 10 switches opens the lock.
The four-state champion stops on a blank tape.
Counting in binary stops.
These claims are about the toy machines above. Real claims, decided in your tab: published numbers and bounds, checked by the claim checker itself.