Kristina Armitage and Nico Roper/Quanta Magazine
Introduction
Staff Writer July 2, 2024 computability computer science computer-assisted proofs games mathematics patterns proofs Turing machine All topics
Once upon a time, over 40 years ago, a horde of computer scientists descended on the West German city of Dortmund. They were competing to catch an elusive quarry — only four of its kind had ever been captured. Over 100 competitors dragged in the strangest creatures they could find, but they still fell short. The fifth busy beaver had escaped their clutches.
Of course, that slippery beast and its relatives aren’t actually rodents. They’re simple-looking computer programs that take a surprisingly long time to run. The search for these unusually active programs has connections to some of the most famous open questions in mathematics, and roots in an unsolvable problem as old as computer science itself. That’s precisely what makes the hunt so compelling. Three of the Dortmund participants summed up the prevailing attitude in a postmortem report (opens a new tab): “Though we know we cannot win the war against the mathematical law, we would like to win a battle.”
The spiritual sequel to the Dortmund hunt began two years ago, when a graduate student named Tristan Stérin (opens a new tab) launched a website announcing the Busy Beaver Challenge (opens a new tab). This time, the participants would cooperate, and everyone was welcome. Over time, the online community grew to include more than 20 contributors (opens a new tab) from around the world, most of them without traditional academic credentials.
Today, the team declared victory (opens a new tab). They’ve finally verified the true value of a number called BB(5), which quantifies just how busy that fifth beaver is. They obtained the result — 47,176,870 — using a piece of software called the Coq proof assistant (opens a new tab), which certifies that mathematical proofs are free of errors.
“The sociological and mathematical engineering that they’ve done to get this far is really impressive,” said Cristopher Moore (opens a new tab), a computer scientist at the Santa Fe Institute.
“I’m surprised how fast they did it,” said Damien Woods (opens a new tab), a computer scientist at Maynooth University in Ireland and Stérin’s adviser. “That’s really like Usain Bolt territory.”
The search for the busy beaver is ultimately a trophy hunt. The specific value of BB(5) doesn’t have applications in other areas of computer science. But for busy beaver hunters, the hard-fought victory over mathematical impossibility is its own reward. It may be the last battle they’ll ever win.
To Halt or Not to Halt
The programs that interest busy beaver hunters aren’t written in any ordinary programming language — they’re instructions for venerable (and theoretical) computers called Turing machines. The pioneering computer scientist Alan Turing conceived of these hypothetical devices in 1936 as a way to mathematically model the process of computation.
Turing machines perform computations by reading and writing 0s and 1s on an infinite tape divided into square cells, using a “head” that operates on one cell at a time. Every machine has a unique set of rules that governs its behavior.
Each of these rules specifies what the head should do when it moves into a new cell, depending on whether it encounters a 0 or a 1 already there. This means a Turing machine’s instructions can be summarized in a table with one row for each rule and two columns (one for when the head encounters a 0 and the other for when it encounters a 1). One rule might be, “If you read a 0, replace it with a 1, move one step to the right, and consult rule C,” in the first column, and “if you read a 1, leave it unchanged, move one step to the left, and consult rule A,” in the second. This is what all the rules look like, except for one special rule that tells the machine when to stop running. (You can play around with Turing machines using an interactive simulator (opens a new tab) on the Busy Beaver Challenge website.)
Share this article (opens a new tab) Newsletter Get Quanta Magazine delivered to your inbox Recent newsletters (opens a new tab)
Kristina Armitage/Quanta Magazine
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.
This three-rule Turing machine halts after 11 steps. Kristina Armitage/Quanta Magazine; Rui Braz for Quanta Magazine; source: Justin Blanchard
Others fall into infinite loops that are easy to spot.
This three-rule Turing machine quickly enters an infinite loop. Kristina Armitage/Quanta Magazine; Rui Braz for Quanta Magazine; source: Iijil
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 (opens a new tab), Radó used these groups to define what he called the “Busy Beaver game.”
In 1962, Tibor Radó invented the busy beaver game by reformulating a famously unsolvable problem about the behavior of Turing machines.
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 (opens a new tab), 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.”
Allen Brady developed busy beaver hunting techniques throughout the 1960s and determined the value of the fourth busy beaver number in 1974.
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.
The SDS 920 was a powerful computer in the early 1960s. As a graduate student, Brady had to drive 90 miles to Beaverton, Oregon, to run his busy beaver hunting program on one.
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 (opens a new tab) in 1965, less than a year before Radó’s death.) Undaunted, Brady pressed on and wrote a dissertation (opens a new tab) 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 (opens a new tab) 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 (opens a new tab) 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 (opens a new tab) 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 (opens a new tab) 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 (opens a new tab) 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 (opens a new tab) 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.
Georgi Georgiev, also known as Skelet, classified all but 43 five-rule Turing machines in 2003. The holdouts, notoriously difficult to analyze, were named Skelet machines in his honor.
In 2003, Georgiev posted his results online (opens a new tab) 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 (opens a new tab) about busy beavers by the computer scientist Scott Aaronson (opens a new tab). Stérin was instantly transfixed. After collaborating with Woods on a paper (opens a new tab) 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.”
In 2022, Tristan Stérin initiated the Busy Beaver Challenge, an online collaboration to conclusively determine the value of the fifth busy beaver number. “I definitely could never have done this on my own,” he said.
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 (opens a new tab), 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 (opens a new tab), 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 (opens a new tab) 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.
Kristina Armitage/Quanta Magazine; source: Busy Beaver Challenge (busy beaver (opens a new tab), #7410754 (opens a new tab), #14263231 (opens a new tab))
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 (opens a new tab) and separate chat server (opens a new tab) 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 (opens a new tab). 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.”
Shawn Ligocki has been interested in the busy beaver search since 2004, when he was a freshman in college. He introduced the Busy Beaver Challenge team to a promising 30-year-old technique called the closed tape language method.