BB(5): the busy beaver and a computer-checked proof

Here’s a Python function that takes a description of a Turing machine and runs it:

def run(rules, max_steps):
    tape, pos, state, steps = {}, 0, "A", 0
    while state != "H" and steps < max_steps:
        write, move, state = rules[(state, tape.get(pos, 0))]
        tape[pos] = write
        pos += 1 if move == "R" else -1
        steps += 1
    return steps, sum(tape.values())

That’s the whole thing. A tape of 0s and 1s, infinite in both directions (a dict that defaults to 0 is close enough), a head that sits on one cell, and a current state. At each step the machine looks at its state and the symbol under the head, and a table tells it what to write, which way to move, and which state to go to next. There’s one extra state, H, that means halt.

Give it the five-state machine that Heiner Marxen and Jürgen Buntrock found in 1989, start it on a blank tape, and it halts after 47,176,870 steps, having written 4,098 ones. On my laptop that takes about ten seconds in plain Python, and along the way the head wanders over about 12,300 cells, almost all of them to the left of where it started.

As of July 2nd, we know that’s the record. No five-state machine that halts runs for longer. That’s BB(5) = 47,176,870, and it was proved by a group of mostly amateur collaborators on a forum called the Busy Beaver Challenge, with the final proof written in Coq by a contributor who goes by mxdys and checked by Coq experts to make sure the formal statement says what it’s supposed to. Quanta had a long piece on it the same day, and Scott Aaronson, who’s been writing about busy beavers for years, wrote about it on his blog. I’ve read both, and the bbchallenge announcement, more than once, and this post is my attempt to explain why I think it’s one of the nicest results in a while.

The game

Tibor Radó defined the busy beaver function in 1962. Take every Turing machine with n states (plus the halt state) and two symbols, start each one on a blank tape, and throw away the ones that never halt. Of the ones that do, which runs the longest? Radó had two versions: Σ(n), the most 1s left on the tape, and S(n), the most steps. People now usually write BB(n) for the step count, so BB(5) = 47,176,870 and Σ(5) = 4,098.

Small cases are easy. With one state, the best you can do is write a 1 and halt, so BB(1) = 1. With two states, the champion takes six steps. Here’s the whole run:

BB(3) = 21 and BB(4) = 107. Those were settled by 1983, the second by Allen Brady, with a lot of hand analysis. Then 107 jumps to 47 million at five states, and the six-state record that people know of is a number so large that you need towers of exponents to write it. BB grows faster than any function you could write a program for, which is a fact you can prove, and it’s the fun part.

Why it’s the halting problem in miniature

Suppose you knew BB(5). Then you could tell whether any five-state machine halts: run it for 47,176,870 steps. If it hasn’t halted by then, it never will, because if it did, it would be a five-state machine running longer than the longest one. So knowing BB(n) solves the halting problem for n-state machines.

Turn that around. Turing showed in 1936 that no program decides halting for all machines. If BB(n) were computable by some program, you could compute it for any n and solve halting for everything, so BB can’t be computable. That’s a much stronger statement than “hard to compute”: no program computes it for all n, ever. The only way to get a value is the way the bbchallenge people did, one n at a time, by actually deciding whether every single machine of that size halts.

For n = 5 that’s a finite job. There are a lot of five-state machines, but after you throw out the ones that are the same machine with states renamed, or the mirror image of another one, and some other easy symmetries, the announcement says you’re left with about 180 million. For each one you need a proof: either it halts within 47,176,870 steps (run it and see) or it never halts. The never-halts part is where the whole difficulty lives.

Proving a machine never halts

The project’s approach is a collection of “deciders”, programs that each recognize one kind of non-halting behavior and produce a reason it never halts.

The simplest kind is a machine that gets into a loop: the same state, the same head position and the same tape contents as some earlier step. It’s going to do the same thing again, forever. A slightly cleverer decider catches machines that repeat a pattern while drifting along the tape, the same local picture but shifted a few cells to the right each time. Then there are machines that count, writing what amounts to a binary counter on the tape and incrementing it forever, and machines whose tape can be described by a regular language that you can show is closed under the machine’s steps (that’s the finite-automata reduction, one of the deciders the announcement credits). Each decider is a small theorem in disguise. If the machine has property P, it never halts, and here’s a certificate that it has P.

Running the deciders in sequence knocks out nearly everything. What’s left after that is a short list of really nasty machines. In 2003 Georgi Georgiev, known as Skelet, wrote a program that he said decided every five-state machine except 43, and those 43 holdouts have been the famous problem cases since. The bbchallenge team ended up proving a handful of machines individually, including two of Skelet’s, #1 and #17, which were the hardest. I’d love to tell you how those proofs work, but I’ve read the forum threads and I’ll admit I followed the outline and not the details.

Why Coq

This is the part I find most interesting as a programmer.

If you’ve read my post about the 200-terabyte proof, you’ll remember the trick there: the SAT solver was big, clever and probably buggy, so it logged its reasoning in a format a small, simple checker could verify. You didn’t trust the solver. You trusted the checker, which you could read in an afternoon.

The busy beaver proof has the same problem with more moving parts. Dozens of deciders, written over two years by different people in different languages, with fiddly code for things like the tape representation and the symmetry reduction. Any bug in any one of them, a decider that wrongly says “never halts” about a machine that does halt after 50 million steps, and the result is wrong. And a wrong result here would be very hard to spot, because what you’d be missing is a machine nobody has seen.

So the final proof is the deciders themselves, written in Coq and proved correct in Coq. Coq is a proof assistant: you write definitions and theorems, you write proofs, and a small kernel checks every step. The statement at the top is roughly “the maximum number of steps over all halting five-state, two-symbol Turing machines started on a blank tape is 47,176,870”, with “Turing machine” and “halting” defined in a few lines in the same file. Everything else, the enumeration, the symmetry argument, every decider, has to be proved to do what it says, or Coq won’t accept it.

That’s why they had independent Coq people read the statement. The thing you have to trust is that the definitions at the top mean what we think they mean, plus Coq’s kernel, which is small and has been looked at very hard by a lot of people. You don’t have to trust any of the deciders, or anyone’s code, or me. The announcement says the proof compiles in about ten hours on a laptop, which means anyone who cares can check it. I haven’t, yet. I’d like to, mostly so I can say I have.

It’s also different from the 200-terabyte proof in a way I like. That proof was a giant certificate nobody would ever read, for a problem with no structure anybody understood. This one is still a computer proof, but the pieces are ideas, each decider is a reusable technique, and you could teach a class about them. It’s closer to the four color theorem, which was proved by computer in 1976 and then re-proved in Coq by Georges Gonthier in 2005, than to a brute-force search.

Who did it

Something I didn’t expect when I started reading: most of the people involved aren’t professional mathematicians. The challenge was started in 2022 by Tristan Stérin, and the contributors are a mix of programmers, students and hobbyists, many of them known only by handles. Some of the critical work, including the Coq proof, came from people whose real names aren’t in the announcement. That’s how a lot of open source works, and I’ve never seen it be how a forty-year-old math problem gets solved.

I did a math degree and then spent most of my career writing software, and I’ve occasionally wondered whether those two things have much to do with each other day to day. This is the most direct answer I’ve seen. The proof is software, it’s correct because a program checks it, and it was built the way we build software, by a lot of people on a forum, with issues and pull requests.

What’s next

BB(6) is a different universe. The best six-state machine found so far, by Pavel Kropitz in 2022, runs for more than 10↑↑15 steps, which is a tower of fifteen 10s. And on the bbchallenge forum people have already found six-state machines whose long-term behavior comes down to questions like the Collatz conjecture, where nobody has any idea how to prove anything. If one of those is in the way, BB(6) isn’t going to be settled by a better decider, it’s going to need new mathematics, and maybe not in my lifetime.

And it gets worse further out, in a way that’s provable. In 2016 Adam Yedidia and Scott Aaronson built a Turing machine with 7,918 states that halts if and only if the standard axioms of set theory (ZFC) are inconsistent. If ZFC is consistent, which is what nearly everyone assumes, it can’t prove that about itself, so it can’t prove that machine never halts, and so it can’t pin down BB(7,918). People have pushed that number down a lot since, to below 800 states. Somewhere between 6 and a few hundred, the busy beaver numbers stop being things our mathematics can know at all.

Five was the last one where a determined group with a forum, a proof assistant and two years could get there. I’m glad they did, and I’m going to spend part of a weekend trying to read through the deciders, starting with the simplest ones.