In a mysterious realm of computer science, a forty-year-old conundrum known as the Busy Beaver problem has recently been cracked by a group of amateur enthusiasts. This achievement has not only caused a stir in the academic community but has also earned recognition from renowned mathematician Terence Tao, who shared the news on social media and emphasized the importance of proof assistants in mathematical research.
Computer scientist Scott Aaronson also highly praised this discovery, considering it the most significant advancement in the study of the Busy Beaver function since 1983. This achievement marks a deeper understanding of the boundaries of computational theory and showcases the potential of software-assisted proofs in solving complex mathematical problems.
The Busy Beaver problem originated in Dortmund, Germany, over 40 years ago when computer scientists sought to find a specific Turing machine that could write the most "1"s before halting. Turing machines, an abstract computational model proposed by Alan Turing in 1936, perform calculations by reading and writing 0s and 1s on an infinitely long tape.
After the fourth Busy Beaver number was determined in 1974, finding the fifth became an unresolved issue. Now, an online community consisting of over 20 contributors from around the world has successfully verified that the fifth Busy Beaver number BB(5) is 47,176,870 using Coq, a proof assistant software.
This achievement has not only excited the community but also amazed computer scientist Damien Woods, who compared this progress to Usain Bolt's speed. Although the solution to this problem may not have direct applications in other areas of computer science, for the participants, the struggle against mathematical impossibility itself is the greatest reward.
The core of the Busy Beaver problem lies in understanding the behavior of Turing machines, particularly their performance on the halting problem. The behavior of Turing machines is defined by a set of rules, which can be imagined as a table. Each rule specifies the actions to be taken by the read-write head when it encounters a 0 or 1 in a specific state.
Although Turing machines may fall into infinite loops, determining whether they will halt is a famous unsolved problem. Mathematician Tibor Radó was dissatisfied with this conclusion and thus invented the "Busy Beaver game," exploring the essence of the halting problem by grouping Turing machines according to the number of rules they possess.
Early researchers like Allen Brady explored this problem by writing programs to simulate the behavior of Turing machines. Their work and findings laid the foundation for later explorers.
By 2022, graduate student Tristan Stérin had initiated the "Busy Beaver Challenge," an online collaborative project aimed at ultimately determining BB(5). With innovative methods and the help of Coq, the team eventually succeeded in finding the fifth Busy Beaver.
This achievement is not only a challenge to mathematical impossibility but also an exploration of the limits of computer science. With the confirmation of BB(5), researchers are drafting an academic paper, which will be a human-readable version supplementing the Coq proof. At the same time, they are also considering whether the exploration of BB(6) will be the next goal.
Reference: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/