The busy beaver problem, a computer science problem that has lasted for forty years, has finally been solved by a group of amateurs! This breakthrough development not only shocked the academic community, but was also recognized by the famous mathematician Terence Tao, and was hailed as the most important development in this field since 1983. Using the Coq proof assistant, they successfully verified that the value of the fifth busy beaver number BB(5) is 47,176,870, demonstrating the great potential of software-assisted proof in solving complex mathematical problems, and also providing us with insights into Turing machine behavior and halting problems. new perspective.
In a mysterious area of computer science, a forty-year-old problem called the busy beaver problem has recently been successfully solved by a group of amateurs. This achievement not only caused a sensation in the academic world, but was also recognized by the famous mathematician Terence Tao, who forwarded the news on social media and emphasized the importance of proof assistants in mathematical research.
Computer scientist Scott Aaronson also spoke highly of this discovery, believing it to be the most important development in busy beaver function research since 1983. This achievement marks a deep understanding of the boundaries of computational theory and demonstrates the potential of software-assisted proofs in solving complex mathematical problems.
The busy beaver problem originated more than 40 years ago in Dortmund, Germany, when computer scientists tried to find a specific Turing machine that could write the most 1's before stopping. A Turing machine is an abstract computing model proposed by Alan Turing in 1936 that performs calculations on an infinitely long magnetic tape by reading and writing 0s and 1s.
After the fourth busy beaver number was determined in 1974, finding the fifth beaver became an open question. Now, an online community of more than 20 contributors from around the world, using proof assistant software called Coq, has successfully verified that the fifth Busy Beaver number BB(5) has a value of 47,176,870.
This achievement not only excited the community, but also aroused the amazement of computer scientist Damien Woods, who likened the progress to the speed of Usain Bolt. Although the solution to this problem may not be directly applicable to other areas of computer science, for the participants, this struggle against mathematical impossibility is the greatest reward in itself.
The core of the busy beaver problem lies in understanding the behavior of Turing machines, specifically their performance on halting problems. The behavior of a Turing machine is defined by a set of rules, which can be imagined as a table. Each rule specifies an action that should be performed when the read/write head encounters a 0 or a 1 in a specific state.
Although Turing machines can get stuck in infinite loops, determining whether they ever stop running is a famously unsolved problem. Mathematician Tibor Radó was not satisfied with this conclusion, and thus invented the "busy beaver game" to explore the nature of the halting problem by grouping Turing machines according to the number of rules they had.
Early researchers, such as Allen Brady, explored this problem by writing programs to simulate the behavior of Turing machines. His work and the discoveries of other researchers laid the foundation for later explorers.
Until 2022, graduate student Tristan Stérin launched the Busy Beaver Challenge, an online collaborative project aimed at finalizing BB(5). Through innovative methods and the help of Coq proof assistant, the team finally succeeded in finding the fifth busy beaver.
This achievement is not only a challenge to the impossibility of mathematics, but also an exploration of the limits of computer science. With BB(5) confirmed, the researchers are drafting an academic paper that will be a human-readable version that complements the Coq proof. At the same time, they are also thinking about whether the exploration of BB(6) will become the next target.
Reference: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
The solution to the busy beaver problem is not only a major breakthrough in the field of mathematics, but also provides new directions and ideas for future computing theory research. This achievement encourages more people to participate in the research of mathematics and computer science and explore unknown areas together.