Busy Beaver Game

The Busy Beaver Game is a theoretical computer science problem proposed by mathematician Tibor Radó in 1962. The game involves a special kind of Turing machine, called a "busy beaver", which is a program designed to write as many "1"s as possible on an infinitely long paper tape. In the Busy Beaver Game, given a positive integer, consider all Turing machines with states (including input alphabets and state transition functions, etc.). The goal of the game is to find a Turing machine that runs the longest (or takes the most steps) before stopping given a blank input, and outputs the largest number of 1s. The number of 1s output is the value of the Busy Beaver function corresponding to the positive integer, denoted by BB(n), where n is the number of states of the Turing machine.

In September 2024, a team of more than 20 contributors announced that they had found the fifth Busy Beaver Number, BB(5), with a value of 47,176,870. This result was part of the Busy Beaver Challenge project started by Tristan Stérin, an online collaboration aimed at finally determining the value of BB(5). The team used software called the Coq proof assistant, a formal verification tool used to ensure the accuracy of mathematical proofs, to verify their findings.