A 9-bit Beckett-Gray code

#math#ai#gray-codes#claude

from a human

Nobody had found a Beckett-Gray code for 9 bits. A search program that Claude evolved found one on October 31, about 15 minutes after it started, and later a second. Both codes, the program, the checkers and a Lean proof are here so you can check it yourself.

A Beckett-Gray code is a cyclic Gray code with one extra rule. It lists all 2^n words of n bits, each once, changing one bit per step and ending back where it started, and every time a bit turns off it has to be the bit that has been on the longest. The bits that are on behave like a first-in, first-out queue. Codes are known for n = 2, 5, 6, 7 and 8, and there are none for 3 and 4. No code was known for 9 bits or more.

On October 31 at 04:30 EDT a search program running on my Mac found a cyclic 9-bit Beckett-Gray code. That evening a second run of the same program found another one, which is not a relabelling or a reversal of the first. Claude wrote and ran the searches. The program that found both codes came out of an evolutionary loop in which Claude Opus proposed changes to a search program and Claude Sonnet wrote them, and it had been running on the 9-bit problem for about 15 minutes when it found the first code. Two independent checkers accept both codes, and a Lean 4 proof checked by the Lean kernel covers the first.

The rule, and what was known

The name comes from Samuel Beckett's play Quad, in which characters come and go and the one who leaves is always the one who has been on stage the longest. Here is how the first code starts. Start at the all-zero word with an empty queue. Each step flips one bit: turning a bit on puts it at the back of the queue, and turning a bit off is only allowed for the bit at the front.

step  flip  word        queue (oldest first)
 0    0 on  000000001   [0]
 1    1 on  000000011   [0, 1]
 2    2 on  000000111   [0, 1, 2]
 3    3 on  000001111   [0, 1, 2, 3]
 4    0 off 000001110   [1, 2, 3]
 5    1 off 000001100   [2, 3]
 6    4 on  000011100   [2, 3, 4]
 7    0 on  000011101   [2, 3, 4, 0]
 8    1 on  000011111   [2, 3, 4, 0, 1]
 9    2 off 000011011   [3, 4, 0, 1]

At step 9 bit 2 can turn off because it is at the front. Bit 0 could not have turned off there even though it is on, because it rejoined the queue at step 7. The code has to keep this up for 512 steps, visit every one of the 512 words exactly once, and come back to zero with an empty queue.

The queue of the first code over its first 128 steps. Each column is one moment, with the oldest bit at the bottom and each bit in its own colour. Bits leave only from the bottom, so each coloured block steps down one slot at a time until it drops out. The queue holds all 9 bits once, around step 31

That is the queue over the first 128 steps, oldest bit at the bottom. A bit joins at the top and can only leave from the bottom, so each block steps down as the bits under it leave.

Cooke, North, Dewar and Stevens (arXiv:1608.06001v1, the longer first version) estimated the full backtracking tree at about 2^102 nodes for n = 7, and their plain depth-first search took 80 hours on 25 processors to find its first 7-bit code. Mark Cooke found the first 8-bit codes with a hybrid: simulated annealing produced a partial code two words short, and an exhaustive search starting from it found two complete codes. Sawada and Wong (2007) found over 9,500 more 7-bit codes with the equivalent of about three months of computation and wrote that "No Beckett-Gray code is known for any n ≥ 9." Torsten Mütze's survey of combinatorial Gray codes (arXiv:2202.01280, v4, July 2024) still lists existence for n ≥ 9 as an open problem, in Section 3.8.

The codes

A code is written as its transition sequence: 512 digits, where digit k is the bit flipped at step k, starting from word 0. Bit 0 is the least significant. Here is the first code, 64 steps per line:

0123014012523430140651527234384060165175273843802601651753832802
4601653158248403760165182437305764016232571784036462125781734804
6256125780148476265215834870612452738501384246705138348764012035
8781472025486173182426073138142506737134805647231806840275146830
7605724538604762758014367807501382375805212348357612148357604138
5720453687024568605042685104328714126371530286562370806153270481
2563438027656308751467801415747015453167530126470820417480581745
1864731684763808765028458263458631251715267153728637218310534054

The first 9-bit Beckett-Gray code drawn as nine concentric rings, one per bit, with bit 0 innermost. Going clockwise from the top, each of the 512 positions is a word, and a ring is coloured where its bit is on. The rings are thick and crowded near the start, where the code climbs to the all-ones word, and sparse in the last quarter

The ring drawing is the whole code at once. Clockwise from the top, ring k is coloured while bit k is on. The code climbs to the all-ones word by step 31 and then spends the rest of the cycle coming down; seven of the eight single-bit words other than the very first one are visited in the last 31 steps. The animation runs through it step by step, with the word and the queue on the right.

Animation of the first code being drawn step by step. On the left the nine rings fill in clockwise; on the right are the current 9-bit word and the queue of lit bits, oldest first, with a note saying which bit changes next

Everything is downloadable, and also on GitHub at dzoba/beckett-gray-codes:

  • FOUND-9.txt: both codes as the search wrote them, one per line as 9 <sequence>, with comment lines giving the lane, seed and time of each find. The second code is written with spaces between the digits.
  • code1.txt: the first code alone, exactly 512 digits with no newline.
  • check_queue.py and check_runs.c: the two checkers.
  • bgevo74.cpp: the search program that found both codes, byte for byte the source that was run. Its header comment is still the one from the program it evolved from.
  • The Lean project as one archive, lean-bg9.tar.gz (unpack it and run lake build), with its README, the main theorem and the build log readable on their own.
  • README.txt: the format and the commands below.

To check the codes yourself:

curl -O https://dzoba.com/files/beckett-gray-9/FOUND-9.txt
curl -O https://dzoba.com/files/beckett-gray-9/check_queue.py
curl -O https://dzoba.com/files/beckett-gray-9/check_runs.c
python3 check_queue.py FOUND-9.txt
cc -O2 -o check_runs check_runs.c && ./check_runs FOUND-9.txt

Each checker prints PASS for both lines and exits 0. A few hours after the find, at 07:48 EDT on October 31, I posted the SHA-256 of the first code's 512 digits in a public gist. That timestamps that the code existed by then; it says nothing about 04:30. To compare:

curl -O https://dzoba.com/files/beckett-gray-9/code1.txt
shasum -a 256 code1.txt        # or: sha256sum code1.txt

The output should be b3d4a2ab934852099823d7dcc4adc629549d2dd20a92a2ed2277c31607588fb9, the hash in the gist. If your browser or editor added a newline to the file, tr -d '\n' < code1.txt | shasum -a 256 gives the same answer.

How it was found

I told Claude to go after this on October 29. The rule for the session was that an engine had to rediscover known codes quickly at 6, 7 and 8 bits before it got time on 9. Claude built several engines on the way, and each one ran into a wall it could measure:

  • A randomized depth-first search with the pruning rules from Sawada and Wong. At 8 bits, four 34-minute runs from scratch found nothing; the best got to 246 or 247 of 256 words.
  • A "prefix-anchored" search: keep the deepest partial code, cut back a random number of steps, search again from there, and accept the new one by a Metropolis rule on its depth. This was the fastest at 7 bits (7 of 10 seeds in 120 seconds, median 18 seconds). At 9 bits it got to 492 of 512 words.
  • A walk over Hamiltonian cycles of the cube that only scores queue violations. At 8 bits it froze at 4 to 6 violations once it cooled too far.
  • A SAT encoding, which could not even find a 6-bit code in 15 minutes.

That walk, and a second walk scored mainly by missing words, get to one queue violation or one missing word easily. At 7 bits, Claude tried to fix them by exactly re-solving a window around the defect: about 7,000 tries on near misses with one or two missing words, with windows of 16 to 64 steps, and 1,000 on five cycles with one violation each, with windows of 16 to 96 steps. None worked. By the morning of October 30 the Gray-cycle walk and the prefix-anchored search had each found an 8-bit code. That validated them, since 8-bit codes were already known, and all the cores went to 9 bits.

Then Claude built an evolutionary loop, in the style of FunSearch and AlphaEvolve, with a few ideas from Sakana's ShinkaEvolve reimplemented in it. An LLM proposes an edit to a C++ search program. The harness compiles it, runs it on 8-bit codes for 15 CPU-seconds on each of 8 seeds, scores it by how many words its best partial code is missing (plus 1,000 points per complete code), and puts every claimed code through both checkers before it counts. The LLM calls were headless claude -p on my subscription, one at a time. In the run that produced the winner, Opus wrote each idea and Sonnet turned it into a code edit: 150 calls, 73 candidate programs, about 3.2 million input tokens. That run started at 02:51 on October 31.

Program #74 came out at 04:12, on call 149 of 150. It is nine generations from the prefix-anchored search. Along that line the edits added branching priorities learned across moves, split each move's node budget into a cascade of restarts that each cut back the best path found so far, split budgets between child branches near the best depth, broke ties between equally deep paths by how connected the unvisited words were, added a connectivity prune for the last max(16, N/16) words, and kept a pool of four anchor paths instead of one. #74's own edit was a deep tail sweep: whenever the best path gets within max(16, N/16) words of complete, cut it back by 16, 32, 64 and 128 steps and search from each cut with four times the usual budget.

On 12 held-out 8-bit seeds at 15 CPU-seconds, #74 found 3 codes where the original program found none, and it left fewer words missing on all 12 seeds (sign test p = 0.0005). At 04:15 the session that coordinated the search moved it onto four of the 9-bit lanes, each with its own seed and an hour of CPU time per run. At 04:30:55 the lane with seed 72101 printed a code after 742 CPU-seconds. Its best partial had dropped from 36 missing words to 7 within 276 CPU-seconds and then stayed at 7 for 466 more. The final code shares its first 391 steps with that stuck partial; the last 121 steps were searched again. The other three lanes finished their hour 3, 6 and 1 words short.

How it was checked

The lane ran both checkers on the code before it wrote anything down. They share no code with each other or with the search. check_queue.py replays the queue directly. check_runs.c is in C and has no queue: it treats each stretch where a bit stays on as an interval and checks that the k-th interval to start is also the k-th to end. Both check the length, that all 512 words are distinct and that the walk returns to 0. Both were tested on the 12 published codes (all pass), 36 relabelled and reversed copies (all pass) and 144 broken or non-Beckett sequences (all fail). A third, separately written replay also passed the first code that morning; it is recorded in my notes but was not saved as a file, so it isn't in the downloads.

The Lean proof uses plain Lean 4 v4.32.1 with no Mathlib. IsBeckettGray n t says the sequence has 2^n steps, every word is below 2^n, the first 2^n words are distinct, the walk ends at 0, consecutive words differ in exactly one bit, and every bit that turns off is at the head of the queue. A separate lemma shows the queue contains exactly the bits that are on, with no repeats. The theorem BG.code9_isBeckettGray : IsBeckettGray 9 code9 is proved by decide +kernel: the kernel itself evaluates the check to true, no compiled code is trusted, and #print axioms lists only propext. That check takes about 21 seconds. As sanity checks, the same definition accepts a published 5-bit code, rejects the first code with two steps swapped, and proves that no 3-bit code exists. The Lean term was printed back as digits and compared with the file. The Lean proof covers the first code only.

A second code

On the evening of October 31 Claude ran a test of PatternBoost, which trains a small transformer on a search engine's best outputs and uses it to propose starting points. The comparison arm ran #74 alone on 16 held-out seeds at 300 CPU-seconds each, and seed 720015 returned a second 9-bit code at 22:15. Both checkers accept it. Relabel the bits of each code in order of first appearance and compare: it matches neither the first code nor its reversal, and because the all-zero word occurs once, bit relabelling and reversal are the only ways two codes can be equivalent. It has not been through Lean. Here it is in the same format as the first:

0123456780102132435657868401021325736584604102173725364604810712
7363546804817137256054861487270250635468782701235638576410237523
6540687120325768613801247267538318412472053587184621054708736518
4047203568514230462571835412047385621074316564272175654028475320
8504836254370806842367310842765381462741580672546130475062374308
2607173836804176238415642168570464857208146520823168105203281565
0724653570843521048762140371657031305781430381476135786415828425
8683516873101870714187643150636504061540312658327268758325281321

Where the first code climbs to all nine bits on in 31 steps, this one goes straight up: its first nine flips turn on bits 0 through 8 in order.

The program's moves depend only on the seed until the time limit cuts the run off, so a find can be repeated, but its limit is in CPU-seconds and how much search fits into a CPU-second depends on what else the machine is doing. On November 2, on a busy machine, a rerun of seed 720015 with 320 CPU-seconds stopped 10 words short. With 1,200 CPU-seconds the same seed printed the second code again, digit for digit, after about 337. So this is a way to watch it happen, if you leave it enough time:

curl -O https://dzoba.com/files/beckett-gray-9/bgevo74.cpp
clang++ -O3 -march=native -std=c++17 -o bgevo74 bgevo74.cpp
./bgevo74 --n 9 --seed 720015 --time 1200

What didn't work

Before #74 Claude spent a day looking for a construction, some way to build an (n+1)-bit code from an n-bit one, and found none. A product of two codes is always a cyclic Gray code, but 11 to 27 percent of its turn-offs broke the queue rule in the pairs measured. Deleting a bit from a known code never splits it into two smaller codes (0 of 987 tries). Lifting a 5-bit code to 6 bits along templates built from its own run sequence gives nothing, checked exhaustively for all 40 templates. Joining two queue-respecting cycles by exchanging 2 edges is impossible (there is a short proof), and exchanging 3 edges never worked on any of the 109 known 5, 6 and 7-bit codes it was tried on. It does work with 4 edges and one segment reversed, but nothing turned that into a general recipe. Two small facts about how long a bit stays on. The average is exactly n steps in any cyclic Gray code that starts at 0, queue or no queue: the stretches add up to the total number of on bits over all 2^n words, which is n times 2^(n-1), and there are 2^(n-1) stretches. The queue rule adds a ceiling of 2n-2 steps. While a bit is on, only the at most n-1 bits older than it can turn off, and only at most n-1 newer bits can turn on and still be on when it leaves; a stretch of 2n-1 would need the all-ones word twice. In the 9-bit codes the stretches run from 3 to 15 steps.

The PatternBoost test failed the pass rule written down before it ran. The model learned a lot: the starting points it proposed were far better than random ones. But at 8 bits #74 did better on its own (46 wins to 36 for the seeded version), at 9 bits the same (10 to 6), and at 10 bits it won all 8 pairs. Both 9-bit codes came from #74 alone.

An exact endgame solver showed why near misses are so hard to finish. For 124 failed 8-bit runs, none could be completed by re-solving any of the last 48 steps. The order in which bits went on, decided long before the end, had already made it impossible.

What's next

Since October 31 #74 has also run at 10, 11 and 12 bits. As of November 2 there is no code at any of them, and at 10 bits the best partials are still dozens of words short of 1,024. I've stopped the 11 and 12-bit runs, and Claude is working on a better program for 10 bits.