During a summer trip to Germany, Ligocki met up with Marxen in Berlin and bonded over the concept of busy beavers. Beer played a role in breaking the language barrier, but Ligocki ended up missing his train back to Hamburg due to overindulgence. This encounter sparked Ligocki’s interest in the busy beaver problem, which he carried with him throughout college.
After graduation, Ligocki’s busy beaver pursuit took a backseat to life’s demands. However, in early 2022, he set up an online discussion group to reconnect with researchers interested in the problem. This led to Stérin inviting him to join the Busy Beaver Challenge, to which Ligocki readily agreed.
One of Ligocki’s contributions to the challenge was reviving Marxen’s “closed tape language method” discussed in a Berlin pub years earlier. This method provided a new way to identify patterns on a Turing machine’s tape that indicate it will never halt, expanding the scope of non-halting machine identification.
Despite the theoretical promise of the closed tape language method, Ligocki struggled to develop a program that covered all cases. Blanchard eventually cracked this challenge, followed by other contributors who optimized the program’s speed. Within a few months, the closed tape language method evolved into a powerful tool capable of handling complex machine patterns.
As new contributors joined the Busy Beaver Challenge, they tackled various machines, including the formidable Skelet #1 and Skelet #17. Ligocki and Kropitz eventually cracked Skelet #1, revealing its intricate behavior after trillions of steps. The community’s collaborative efforts led to breakthroughs on previously unsolved machines, bringing them closer to a comprehensive solution.
A mysterious contributor known as mxdys played a pivotal role by completing a 40,000-line Coq proof for the fifth busy beaver. This proof validated Marxen and Buntrock’s discovery from over three decades ago, marking a significant milestone in the challenge.
While the team works on formal academic papers to document their results, they face new challenges with the sixth busy beaver. The discovery of “Antihydra,” a machine with a halting problem akin to the Collatz conjecture, presents a formidable obstacle that may require a mathematical breakthrough.
As contributors contemplate their next steps, some plan to continue exploring variants of the busy beaver problem, while others pursue different interests. Stérin aims to develop collaborative tools for mathematics research, while Kądziołka explores a passion for the European rail network. Ligocki remains committed to busy beaver hunting, reflecting on the unpredictable nature of the pursuit, much like the halting problem itself.
The Busy Beaver Challenge exemplifies the power of collaboration and perseverance in tackling complex mathematical problems, showcasing the diverse talents of contributors from varied backgrounds. As the team navigates future challenges, their experiences offer valuable insights into the dynamics of collaborative research and the pursuit of mathematical knowledge.
