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.