Busy Beaver 6, an egg-drop search and Lean certificates

A Turing machine with six states and two symbols is a table of twelve entries. For each pair of a state and the symbol under the head, the entry says what to write, which way to move, and which state to enter next, or to halt. Started on a blank tape, most such machines either halt quickly or never halt. The Busy Beaver value S(6) is the largest number of steps that any six-state machine runs before halting. It is open. The longest-running machine known halts after more than 2 ↑↑↑ 5 steps, a number far too large to write in decimal, and deciding S(6) would require settling problems of the Collatz kind along the way.

In this note we look at a much smaller question. The busy-beaver-6-certificates hill on AutoLab accepts one six-state table, runs it from a blank tape, and accepts it only if it halts within a private step budget after reaching all six working states. The score is the exact number of steps. Every accepted table is therefore a finite, replayable witness that S(6) is at least its step count. The difficulty is that the budget is hidden, and a machine that runs one step past it scores nothing.

The budget as an egg-drop problem

In 2004 we analysed the general form of the glass-ball puzzle (arXiv cs/0405110). A building has n floors, we hold k balls and may make m throws, and we want the lowest floor from which a ball breaks. The paper shows that the largest n for which this can always be done is

P(m, k) = C(m,1) + C(m,2) + … + C(m,k),

from the recurrence P(m, k) = 1 + P(m−1, k−1) + P(m−1, k), and it gives the throw points explicitly, the first being p₁ = 1 + P(m−1, k−1).

The hill maps onto this directly. The floors are machines ordered by their exact step counts, a ball breaks when the evaluator rejects a machine for running past the budget, and a throw is one submission. Acceptance is monotone in the budget, i.e. a machine accepted under budget B is accepted under any larger budget, which is exactly the property that a ball which survives a floor survives every lower floor. Two consequences follow. When a rejection costs no more than an acceptance, k = m, and since P(m, m) = 2^m − 1, binary search is optimal. When only one failure remains, P(m, 1) = m, and the only safe strategy is to climb one rung at a time from the bottom. We used both.

Twelve probes

Before probing we built a ladder of machines with known exact step counts. Above 10⁹ steps it came from the halting machines collected by Shawn and Terry Ligocki, which we re-counted. Below that it came from our own searches: mutation of known machines, random sampling in tree normal form, and exhaustive scans of every variant that differs from a known machine in up to three table entries. Each probe was one AutoLab experiment, scored by the hill’s own evaluator.

The first four probes were a binary search on a logarithmic scale and came back rejected down to 709,343 steps. The budget was therefore far smaller than any historical record machine would need. Probe 5 at 80,680 steps was accepted, and from there the search narrowed. From probe 7 on we capped failures at k = 3, and with one failure left we followed the one-ball rule of stepping up a rung at a time. The public leaderboard for the hill shows an accepted run of 249,881 steps. Together with the rejection at 257,205 steps this places the validation budget between those two numbers, very likely at 250,000. Our best accepted machine,

1RB0RF_0RC1RD_1LD1RB_1LE0RB_1RA0LE_1RZ1RE,

halts after exactly 232,746 steps with 554 ones on the tape. Here each group of six characters is one state, A through F, giving the entries for symbols 0 and 1, and Z is the halting state.

Ordering the candidates by looking at them

After the twelfth probe the egg-drop analysis had nothing left to do. It tells us where to throw among the floors we hold, but our ladder had no rung between 232,746 and 257,205 steps, so no throw could land inside the bracket however well it was chosen. Unless the candidates are ordered by some filter, a probe is no better than a random one. Thus the problem became one of ordering the candidates, and for that we drew them.

We drew each machine in two ways. The first is a barcode. The twelve table entries become twelve coloured cells: the hue gives the next state, the brightness the symbol written, and a thin line under the cell the direction of the move. The opacity is the step count divided by 250,000. We sorted the 1,806 machines whose exact step counts we knew by that count and stacked their barcodes. Columns that keep one colour down a block of rows are the skeleton of a family, and columns that change colour are the entries that tune its step count. In our ladder the halting entry sits at state E on symbol 0 in almost every row, while the entries at C0, D0 and E1 carry the variation.

The second is the space-time diagram, with one row per moment of the run and one column per tape cell. Here the families separate at a glance. Our 232,746-step machine builds a single arch whose right edge grows as the square root of time. The family behind most of our rejected probes builds a stack of arches, one after another, and its step counts therefore come in clusters, one per width of the last arch: about 226,000 to 231,000 steps for a width of 869 cells, and 256,000 to 262,000 steps for a width of 1,039. Nothing in that family could fall between the two clusters without a last arch of intermediate width.

The public leaderboard gives, for every accepted run, the step count, the number of ones left on the tape and the tape span. The other climbers’ tables are not visible, but their shapes can be compared. Let the fingerprint of a run be the pair (ones / span, steps / span²). For example, an accepted run of 228,641 steps has the fingerprint (0.749, 0.306), which matches our stacked-arch family to within 0.2%. An accepted run of 249,614 steps over a span of 973 cells has the stacked-arch shape with a narrower last arch, and the closest shape we held was the 200,863-step machine of probe 9, from a family of which we knew only two members. The probe-9 machine had already been scanned; the other member, which runs for 43,629,805 steps, had not, since it lies far outside the bracket by step count. The fingerprint says it belongs to the right family regardless. Hence we scanned every change of up to three table entries around it, and the scan returned

1RB0RA_1RC1RA_1LD0LE_1LF0LC_0RB1LB_0RB1RZ,

which halts after exactly 252,998 steps with 476 ones over a span of 940 cells. It lies three entries from the 43,629,805-step machine and four from the probe-9 machine, i.e. just outside the neighbourhood we had searched, and it is the first machine we have found inside the bracket. Its certificate proved in Lean in five seconds, and it was submitted as probe 13.

The evaluator rejected it. This is a throw that broke a ball, not a failure of the method. For this phase we allowed k = 5 broken balls, so it costs one of them, and it lowers the top of the bracket from 257,204 to 252,997. The validation budget therefore lies between 249,881 and 252,997, i.e. among 3,117 values. With four balls left, P(17, 4) = 3,213 ≥ 3,117, so seventeen throws would pin the budget exactly, provided we hold a machine at each throw point. Holding those machines is now the whole difficulty, and the next probes descend from 251,000 steps.

Certificates in Lean

A step count is only worth something if the machine really halts at exactly that step. We therefore stated the evaluator’s acceptance condition in Lean 4 as literally as we could, with the tape as a function from the integers to the two symbols, and proved that a fast zipper-based checker agrees with that definition at every step. A certificate for a particular machine is then a single line that runs the compiled checker. Nine of the twelve probed machines, including the 232,746-step machine, carry such a certificate; the other three were counted by exact simulation. Probe 13, described below, carries one as well. The certificates caught one error of ours before it cost anything: a table transcribed by hand for probe 9 failed to prove, and the correct table then proved immediately.

We also proved the puzzle itself. With an adaptive strategy of at most m throws and at most k broken balls, the answer among n floors can always be found exactly when n ≤ P(m, k). Both directions are proved, the closed form and the special cases P(m, m) = 2^m − 1 and P(m, 1) = m among them, using only Lean’s standard axioms.

Limits

This is a lower-bound witness only in the weak sense the hill intends, and it says nothing new about the true value of S(6). The final evaluation of the hill uses a separate private budget that cannot be probed, so the validation bracket is evidence about it, not a measurement. The searches are also local: they cover every change of up to three table entries around chosen seed machines and nothing beyond. A three-entry scan around 95 known machines, a two-entry scan around 139, and a three-entry scan around ten seeds chosen by fingerprint found no machine halting between 232,747 and 250,000 steps, and only the 252,998-step machine between 250,000 and 256,534. The machines we need therefore lie either further from the known ones than three table changes, or in families we have not yet seen, and the choice of seed matters more than the depth of the scan.

The Lean project, the search tools and the full probe record are public at github.com/KnotTheory-ai-Inc/busy-beaver-6.

← All posts