With Fifth Busy Beaver, Researchers Approach Computation’s Limits

But just because there’s a way for a Turing machine to halt, that doesn’t mean it will ever actually do so. It could, in the simplest case, get stuck in an endless loop that cycles through a few states. Is there any guaranteed way to tell if a Turing machine with a particular set of rules will halt or run forever? That’s the essence of the halting problem, the famously thorny problem that makes the busy beaver hunt so intoxicating. Turing proved that the halting problem has no general solution — you can never be sure if an approach that works for one machine will work for another.

The halting problem isn’t always hard for specific machines. Some, for instance, halt relatively quickly.

Others fall into infinite loops that are easy to spot.

But spend enough time playing with Turing machines, and you’ll occasionally encounter one that resists this easy classification. Will its journey ever end, or is it doomed to wander the tape forever?

“Until you run it long enough, you’re not going to have any idea what the heck it’s doing,” Moore said. “And how long is long enough?”

Bringing Up Beavers

Beavers enter the story with the mathematician Tibor Radó, who was no stranger to long journeys. Born in Hungary in 1895, he entered university to study civil engineering, but his education was derailed by the outbreak of World War I. Dispatched to the Russian front, he was captured and sent to a prison camp in Siberia, where he began to study mathematics under the tutelage of a fellow prisoner.

After four years, Radó managed to escape. He traveled thousands of miles across the Russian Arctic and eventually made it back to Budapest, where he returned to school and published dozens of math papers in the 1920s, before accepting a faculty job at Ohio State University in 1930. He stayed there for 35 years. Even the wildest journeys sometimes halt abruptly.

Late in life, Radó became interested in the theory of computation. He wasn’t satisfied with Turing’s proof, which involved mind-bending self-referential arguments about the infinite set of all possible Turing machines. To distill the essence of the halting problem into a simpler form, Radó imagined sorting Turing machines into groups based on how many rules they had — one group for all one-rule Turing machines, another for all two-rule machines, and so on. Sure, that leaves infinitely many such groups, since a Turing machine can have any number of rules. But the number of distinct machines in every group is finite, since there are only so many possible combinations of rules. It’s easier to reason about these finite groups than to consider all machines at once. In a 1962 paper, Radó used these groups to define what he called the “Busy Beaver game.”

To play, start by picking a group — that is, the number of rules your machines will have. Feed each machine in the group a tape with 0s in every cell. Some machines will hum along forever. The rest will eventually halt. Of these, some will halt quickly, some will take longer, and one will be the last to stop running. Every group will have a longest-running member, and Radó called these especially industrious machines busy beavers. In the group with n rules, the number of steps that the busy beaver machine takes before halting is the corresponding busy beaver number BB(n). The goal of the game is to nail down the exact values of these numbers.

To succeed, you must determine the runtime of every machine that halts, to see which takes the longest. You must also prove that all the rest never stop. Measuring runtimes is reasonably straightforward, since it’s easy to simulate Turing machines on an ordinary computer. But proving that a machine runs forever amounts to solving the halting problem for it: a specific version of a task that’s certifiably impossible in its most general form.

“We’re playing at this edge of unknowability,” said Shawn Ligocki, a software engineer and Busy Beaver Challenge contributor.

But where exactly does unknowability begin? Turing machines with just a few rules look pretty simple. How hard could it be to understand a program that fits on an index card?

Brady’s Bunch of Beavers

The one-rule case is easy, because there are effectively only two possibilities. If the rule tells the Turing machine to halt when it sees a 0, it stops on the first step. Any other rule will cause the machine to march along the tape forever, since it will encounter a 0 in every cell. That means BB(1) = 1.

Beyond this baby beaver, a hunter armed with only pencil and paper quickly encounters a problem. With two rules, there are already over 6,000 distinct Turing machines to consider; that number swells to millions with three rules, and to billions with four. Working all these cases out by hand is out of the question. “Obviously, you cannot do this,” Ligocki said. “And even if you could, no one would believe you.”

That means this problem rooted in the foundations of computation can only be solved with the help of computers. A fairly simple program suffices to prove that BB(2) = 6. But BB(3) is already much harder to find. Soon after Radó introduced the game, a handful of researchers began the hunt.

One of them was Allen Brady, a mathematics graduate student at Oregon State University. Perhaps inspired by the university’s beaver mascot, Brady set out to see how many of the beasts he could bag. He quickly realized that the key to making progress was to ignore any differences between Turing machines that don’t matter. Consider, for instance, a machine with many rules where the first one tells it to halt if it reads a 0.

“What’s in the rest of those transitions doesn’t matter, because it immediately halts,” Ligocki said. Most of these machines are redundant, as far as the busy beaver game is concerned, so you can rule them all out at once.

Brady integrated this process into a computer program for simulating Turing machines, which constructed a sort of family tree for machines with the same number of rules, based on the similarity of their initial behavior. The program split the tree into multiple branches only when differences between machines became relevant, and lopped off whole branches in which the simulation halted or entered an infinite loop.

Writing this computer program was one thing, but Brady still had to find a computer powerful enough to run it. In 1964 that wasn’t easy. He ended up securing access to a computer in a primate research lab 90 miles away, in a Portland suburb fittingly named Beaverton.

Midway through his work, Brady learned that he’d been scooped: Radó’s graduate student Shen Lin had already proved that BB(3) = 21. (He and Radó would publish the results in 1965, less than a year before Radó’s death.) Undaunted, Brady pressed on and wrote a dissertation that confirmed Lin’s results and made partial progress on BB(4) — a case that Radó had deemed “entirely hopeless.”

BB(4) was difficult not just because of the sheer number of cases, but because four-rule machines are capable of much richer behavior. All two-rule machines that don’t halt get stuck in easily detectable endless loops. In the three-rule case, a few dozen machines run forever without looping. Proving that these machines never halted required different techniques. With four rules, there are thousands of these non-looping machines.

After graduating, Brady identified new species of non-halting Turing machines and gave them fanciful names like shadow trees and tail-eating dragons. In 1966, he discovered a four-rule machine that ran for 107 steps before halting, and he conjectured that it was the elusive fourth busy beaver. He was correct, but it took him until 1974 to prove that no halting machine ran longer. By then Brady had taken up long-distance running himself, competing in marathons around the country while working as a professor of computer science at the University of Nevada, Reno. He wrote up his proof in an internal technical report, and didn’t publish it in an academic journal until nine years later.

It was the last busy beaver number humanity would know for over 40 years.

Take Five

The year Brady published his proof was also the year of the Dortmund competition — the first big hunt for the fifth busy beaver. With five rules, there are nearly 17 trillion possible Turing machines — even just listing them all at a rate of one per millisecond would take over 500 years. Techniques like Brady’s family-tree method that narrowed the search space would be indispensable, but programs would still have to run extremely fast to have any hope of success.

The Dortmund contestants each developed their own beaver search programs and presented the longest-running five-rule Turing machines they could find — the busiest one halted after over 100,000 steps. Coverage of the contest in Scientific American in 1984 introduced the game to a new generation of researchers. One of them soon demolished the Dortmund record with a machine that halted after over 2 million steps.

Among the other new hunters were Heiner Marxen and Jürgen Buntrock, graduate students in Berlin who began working on the problem together in their spare time. They developed new mathematical techniques for accelerating the simulation of Turing machines. But their interest faded after they failed to dethrone the 2-million-step champ. Years later, in 1989, Marxen was working as a programmer at a company that had acquired a powerful new computer, and he decided to dust off his beaver-hunting program. He left it running over the weekend, hoping to reproduce the discovery of the 2-million-step machine. Instead, his program found one that halted after a whopping 47,176,870 steps.

At first he thought there must have been a bug in the code. “After several hours I stopped debugging and started to have a strange feeling,” Marxen wrote in an email. Buntrock soon replicated the result, and they published a paper about it in early 1990, in the heady months that followed the fall of the Berlin wall. In fact, Marxen had caught the busy beaver, but it would take over 30 years to prove that all remaining machines never halted.

In the early 2000s, a Bulgarian computer scientist named Georgi Ivanov Georgiev came tantalizingly close. At the time, he was employed as a systems administrator for the state-owned telecommunications company, and the job demanded little of him. He worked obsessively on BB(5) for two years, spending hours every day refining a computer program that could identify exotic new species of non-halting machines. The final product was 6,000 lines of dense uncommented code, which took over a week to run. It left around 100 Turing machines unresolved. After analyzing those machines by hand, he winnowed the list down to just 43 holdouts.

In 2003, Georgiev posted his results online under the pseudonym Skelet, Bulgarian for skeleton. “As a student I was very thin, and my classmates came up with the nickname,” he explained in an email.

Marxen encouraged Georgiev to keep going, but the two years of intense work had taken their toll. “At the end of this period, I cannot create any new ideas,” Georgiev said. “I was very tired.”

It was a common outcome for busy beaver researchers. For decades, they’d labored alone or in pairs, without much recognition from the broader academic community. It would take a collective effort to finish the job.

Calling All Hunters

That effort began with Tristan Stérin. He became adept at computer programming at an early age after befriending a competitive coding enthusiast on an instant messaging platform in the late 2000s. But he soon realized the culture of programming contests wasn’t a good fit.

“I’m not a competitive person,” he said. “I like to see a problem and think about it for three months rather than having 30 minutes.”

That inquisitive spirit led Stérin from France to graduate school in Ireland, where he worked with Woods on DNA computing, the study of how to implement algorithms using strands of DNA. In the summer of 2020, Woods sent him a survey paper about busy beavers by the computer scientist Scott Aaronson. Stérin was instantly transfixed. After collaborating with Woods on a paper about the capabilities of larger Turing machines, he turned to BB(5), resolving to prove once and for all that Marxen and Buntrock’s 47-million-step machine really was the fifth busy beaver.

“I had the strong intuition that I could not do it myself,” Stérin said. “But I also had the intuition that it could be done.”

From the beginning, Stérin knew that a conclusive proof would have to be well documented and reproducible, because any tiny software bug would be fatal to the whole effort. Georgiev’s program was incredibly sophisticated, but other researchers found it impenetrable.

“When you go back and try to review his code, you just give up,” said Justin Blanchard, a software developer and former math graduate student who joined the Busy Beaver Challenge. Any new approach would effectively have to start from square one.

Stérin decided to build on the traditional approach, but with some tweaks. He would start by using Brady’s family-tree method to eliminate redundant Turing machines and identify which ones halted within 47 million steps. But unlike Brady or his successors, Stérin didn’t include any code to weed out machines that ran forever. Instead, he planned to tackle those using self-contained programs, one for each method of proving a Turing machine will never halt. Dividing the task into pieces this way would make it easier for collaborators to work on each part independently and cross-check their results.

At the end of 2021, Stérin wrote the computer program for the first step. It produced a list of about 120 million Turing machines that would be enough to determine BB(5) — all the rest were redundant. Of those 120 million, roughly a quarter halted before Marxen and Buntrock’s machine, leaving 88 million that were still under consideration.

To help analyze these machines, Stérin built an online interface for visualizing their behavior on “space-time diagrams,” two-dimensional grids of dark and light squares representing 0s and 1s, respectively. Each row in a diagram documents one step in a Turing machine’s evolution. The top row represents the tape after the first step, the second row shows it after the second step, and so on. Viewed this way, the machines in Stérin’s menagerie spring to life, displaying a dizzying variety of different patterns. Establishing that Marxen and Buntrock really had found the fifth busy beaver would mean proving that every one of them ran forever.

That was the part Stérin knew he couldn’t do alone. Plus, he had other obligations — he’d founded a software startup with some friends, and he still had to finish his dissertation. In the spring of 2022, Stérin and a few early converts started a forum and separate chat server on the independent platform Discord. Then it was time to find contributors.

The Busy Beaver Bug

It didn’t take long for Shawn Ligocki to join the team. Perhaps it was fate: He was born in Beaverton in 1985, though he first heard of busy beavers in 2004, at the end of his first semester of college. Over winter break, he started tinkering with beaver search algorithms together with his father, Terry, an applied mathematician at Lawrence Berkeley National Laboratory.

A month later, when Ligocki was back in college and busy with classes, his father called him, excited. He’d decided to test one of their algorithms on a variant of the original busy beaver game invented by Brady, and found a machine that shattered Brady’s record. They reached out to Brady, who’d retired — he was delighted and publicized the result on his website. Shawn Ligocki soon found himself in email correspondence with busy beaver researchers around the world.

“The community was very, very welcoming,” he said. “That’s when I caught the busy beaver bug.”

One memorable encounter occurred while Ligocki was visiting Germany the summer after his sophomore year, when he took a side trip to Berlin to meet up with Marxen. “We got through the language barrier through the medium of busy beavers,” he said. The medium of beer also helped. Ligocki ended up having too many and missed his train back to Hamburg.

The busy beaver bug stuck with Ligocki throughout college, but when he graduated and found a job, life got in the way. He returned to the hunt from time to time, but never for long. In early 2022, he set up an online discussion group to help researchers stay in touch. Then in May, Stérin discovered the mailing list and sent an invitation to join the Busy Beaver Challenge. Ligocki needed no convincing.

One of his first contributions to the project was reviving a technique invented by Marxen, which they’d discussed in that Berlin pub 16 years earlier. Called the “closed tape language method,” it was a new way to identify patterns on a Turing machine’s tape that indicate it will never halt. This is the basic strategy behind programs that identify loopers and many other species of non-halting machines, but the closed tape language method had the potential to identify a much broader class of patterns using a unified mathematical framework.

Ligocki wrote a blog post introducing his new collaborators to the technique, but even though the theoretical idea was very general, he didn’t know how to write a program that would cover all the cases. Blanchard figured out how to do that shortly after joining the project in the fall, but his program was relatively slow. Then two other contributors found ways to make it run much faster. Within the span of a few months, the closed tape language technique had gone from a promising idea to one of their most powerful tools. It could even handle 10 of Georgiev’s 43 holdouts, nicknamed Skelet machines in his honor.

“This thing would never have existed with any one person contributing,” Ligocki said.

A Monster Approaches

As the months passed, new contributors discovered the Busy Beaver Challenge and began chipping away at different parts of the problem. But many machines remained unsolved, and two developed especially fearsome reputations.

The first was Skelet #1, which kept alternating between phases of predictable and chaotic behavior. Then in March 2023, Ligocki and another contributor named Pavel Kropitz developed a series of ideas that finally cracked it open. Using a souped-up version of Marxen and Buntrock’s 30-year-old accelerated simulation technique, they discovered that the tug-of-war between order and chaos did end, but only after more than a trillion trillion steps. Then it finally settled into a repeating cycle that was itself unusually long. Practically all infinite loops begin repeating within 1,000 steps; Skelet #1’s was more than 8 billion steps long.

“Who ordered that?” Blanchard said. “Where did that come from? Why is it here?”

The machine’s behavior was so strange, and the proof combined so many different ideas, that for nearly five months Ligocki wasn’t sure of the result. That period of uncertainty was dispelled by a new contributor — a 21-year-old self-taught programmer named Maja Kądziołka, who mostly goes by the single name mei.

mei grew up in Poland and attended the University of Warsaw for one semester in fall 2021 before dropping out — the rigidity of the curriculum and the move to remote instruction after a surge of Covid-19 cases didn’t fit well with their learning style. They worked at a software company for a little over a year but increasingly found the work draining, and began looking for something more intellectually stimulating. They found it in Coq, the software designed to encode and certify the validity of mathematical proofs.

The Busy Beaver Challenge contributors were already using computer programs in their proofs, but like paper-and-pencil proofs, computer programs are vulnerable to errors. In Coq proofs, the code won’t run unless every line logically follows from the preceding ones, making errors effectively impossible. To mei, figuring out how to craft these proofs began to feel like a game. “It’s almost addictive,” they said. “I started at a normal hour, and then it was night. Then it was morning.”

After learning Coq, mei began looking for an open problem to test it out. That’s when they found the Busy Beaver Challenge. A few weeks later, they’d translated several of the team’s proofs into Coq, including Ligocki and Kropitz’s proof that Skelet #1 never halts — Ligocki could finally be sure about it. Suddenly, an even higher standard of rigor than Stérin’s emphasis on reproducibility seemed possible. And it had all started with someone who had no formal training at all — an amateur mathematician.

“Let’s remember that means a lover of mathematics,” Moore said. “It is not a pejorative term.”

The Dam Breaks

Around the same time, a graduate student named Chris Xu made a breakthrough on the second monstrous machine — Skelet #17. It was usually easy to summarize the behavior of even the most fiendish five-rule Turing machines once you figured out how they worked. “Then you encounter some bullshit like Skelet 17, and you go, ‘Nah, the universe is trolling us,’” mei said. Understanding Skelet #17 by studying the patterns on its tape was like deciphering a secret message wrapped in four layers of encryption: Cracking one code just revealed another totally unrelated code, and two more below that. Xu had to decipher all of them before he could finally prove that the machine never halted.

Xu’s proof was brilliant, but it involved some mathematical intuition that nobody knew how to formalize in the precise terms demanded by Coq. What’s more, the Busy Beaver Challenge’s work wasn’t done: While Skelet #1 and #17 were the two machines that had seemed most formidable, some others remained to be solved, and still more had only been solved using inefficient programs. That was no way to convince the world.

“We wanted to make sure that it was something reasonably reproducible,” Blanchard said, “and also not write a proof where we would say, ‘Step 63: Let this program run for six months.’”

Over the following months, the community slowly cobbled together proofs for the remaining machines, but most had yet to be translated into Coq. Then in April a mysterious new contributor known only by the pseudonym mxdys came in to finish the job. Nobody on the team knows where mxdys is located or any other personal details about them. In a Discord direct message exchange, they mentioned a long-standing interest in mathematical games, but they declined to provide more information about their background.

On May 10, mxdys posted a characteristically succinct message to the Discord server: “The Coq proof of BB(5) is finished.” Stérin replied a minute later with a series of seven exclamation points. In a matter of weeks, mxdys had refined the community’s techniques and synthesized their results into a single 40,000-line Coq proof.

“This is not a thing that’s easy to formalize,” said Yannick Forster, a Coq expert at the French national research institute Inria who reviewed the proof. “I’m still positively shocked.”

The machine that Marxen and Buntrock had discovered over 30 years earlier, which halted after 47 million steps, really was the fifth busy beaver.

“These news are very exciting for me,” Georgiev wrote in an email. “I never expected that this problem would be solved in my time.”

But for another Busy Beaver pioneer, the news came too late. Allen Brady died on April 21, less than a month before the proof was finished. He was 90 years old.

Where Beavers Roam

The Busy Beaver Challenge contributors have begun to draft a formal academic paper describing their results, supplementing mxdys’ Coq proof with a human-readable one. That’ll take a while: Most machines were proved non-halting in multiple ways, and the team will need to decide how best to combine the results into a single proof.

Meanwhile, part of the team has moved on to the next beaver. But just four days ago, mxdys and another contributor known as Racheline discovered a barrier for BB(6) that seems insurmountable: a six-rule machine whose halting problem resembles a famously intractable math problem called the Collatz conjecture. Connections between Turing machines and the Collatz conjecture date back to a 1993 paper by the mathematician Pascal Michel, but the newly discovered machine, dubbed “Antihydra,” is the smallest one that appears unsolvable without a conceptual breakthrough in mathematics. That adds an extra layer of significance to the BB(5) result.

“It’s conceivable that this is the last busy beaver number that we will ever know,” Aaronson said.

There are many variants of the original busy beaver problem, and some Busy Beaver Challenge contributors plan to keep working on these. But not everyone intends to continue this work. They each came to the project on their own, for their own reasons, and their journeys are beginning to diverge.

Stérin wants to develop software tools to facilitate collaborative online projects in other areas of mathematics. “The thing that BB challenge brought me is the deep, deep, deep conviction that it’s an extremely effective way of performing research,” he said. “It deserves to have a bigger stage.”

mei is also pulling back, after developing a fascination with the European international rail network. “I will probably come back to busy beaver things again at some point, but currently it’s not the thing on my mind,” they said. “I’m currently pursuing becoming a train driver.”

Ligocki thinks he’ll keep up his busy beaver hunting, but after 20 years of switching between bursts of intense activity and not thinking about beavers at all, he’s learned not to put too much stock in his predictions.

“It’s kind of like the halting problem,” he said. “You just never can quite tell what’s going to happen.”

Editor’s note: Scott Aaronson is a member of Quanta Magazine’s advisory board.

Correction: July 8, 2024
A previous version of this article incorrectly stated that Pavel Kropitz communicates through Google Translate because he doesn’t speak English. He does speak English; he uses Google Translate to make his messages more idiomatic.