Amateurs Solve a Famous Science Problem On Discord
A team of amateurs recently came together in an online collaboration called the Busy Beaver Challenge to pin down the value of BB(5), the fifth "busy beaver" number, a notoriously difficult problem in theoretical computer science.
2025-04-22 19:00:00 - Quanta Magazine
The busy beaver problem, or “game,” involves finding the Turing machine with a given number of states that runs for the longest series of steps before halting. Using collaborative tools and the Coq proof assistant to verify their work, the team proved that BB(5) equals 47,176,870. The landmark result explores the limits of computation and the boundaries of what is knowable in mathematics.
00:00 - What is the Busy Beaver problem?
01:05 - How does a Turing machine work?
02:35 - Programs that halt versus getting stuck in endless loops: the Halting Problem
04:38 - How to play the Busy Beaver game
05:26 - BB(1), BB(2), BB(3), BB(4) solutions
06:38 - The Busy Beaver Challenge tackles BB(5)
07:31 - The history of the search for BB(5)
08:10 - The Busy Beaver Challenge methodology
08:48 - Coding 'deciders'' to shorten the list of contenders
09:49 - Mysterious contributor confirms BB(5) solution
10:09 - Coq proof of BB(5)
10:54 I- s BB(6) solvable?