How a Group of Amateurs Solved an Impossible Problem

The video explains the Busy Beaver problem, a deceptively simple game about Turing machines that asks for the longest-running program that eventually halts, and reveals that this puzzle is as hard as the deepest open questions in mathematics. It highlights how a decentralized online community, launched as the Busy Beaver Challenge in 2022, managed to solve the fifth Busy Beaver number by reducing trillions of possible machines to a manageable set and using volunteer-written "deciders" plus formal proof assistants to verify the answer. Their success confirmed that a machine halting after 47,176,870 steps is indeed BB(5), a feat once thought impossible for amateurs. The video closes by noting the next frontier, BB(6), is dramatically harder—with nearly 60 quadrillion machines—and that one stubborn machine's behavior is tied to the Collatz conjecture, leaving doubt about whether it will ever be solved, though past doubts offer cautious hope.

• ▶ 0:01 The Busy Beaver problem is a deceptively simple game using only 1s and 0s that asks: what is the longest, most complicated thing a program can do and then stop?
• ▶ 0:29 The problem is not just a curiosity—it is just as hard as the most difficult open problems in mathematics, and recent online amateurs solved a tough version faster than expected.
• ▶ 1:04 Tibor Radó formulated the Busy Beaver game in 1962 based on Turing machines, which use an infinite tape, a read/write head, and a simple instruction table yet can compute anything any program can.
• ▶ 2:22 Programs either halt or run forever; the question of determining which is the case is the halting problem, which is extremely hard to solve.
• ▶ 4:06 The Busy Beaver game fixes N rules, generates a finite set of Turing machines, runs them all, and defines BB(N) as the maximum number of steps a halting machine takes.
• ▶ 5:58 Early values are small (BB(1)=1, BB(2)=6, BB(3)=21), but BB(4) required sorting through billions of machines and was only solved in 1974 by Allen Brady, giving 107 steps.

• ▶ 6:35 Tristan Stérin launched the Busy Beaver Challenge in 2022 to collaboratively tackle BB(5), building tools so many volunteers could contribute to the search.

• ▶ 7:17 The scale of the problem is enormous: with five rules, there are nearly 17 trillion possible Turing machines, raising the question of where to begin.

• ▶ 7:46 Marxen and Buntrock found a five-rule contender that halted after 47,176,870 steps, but they couldn't prove it was the true BB(5), giving later teams a concrete target to beat.

• ▶ 8:18 The team built a database of five-state Turing machines, using Stérin's program to reduce trillions of possible machines to 88 million by removing redundant ones and any that halted before Marxen and Buntrock's record-holder.
• ▶ 8:38 Volunteers wrote "deciders" to prove whether machines halt or run forever, and a decentralized group of ~20 challengers validated them by requiring independent reproduction and formal mathematical write-ups, narrowing the list to about 30 holdouts.
• ▶ 10:08 A pseudonymous contributor, mxdys, used the Coq proof assistant to formalize and verify all the results within one to two months, confirming that Marxen and Buntrock's machine was indeed the fifth busy beaver—a success driven by community collaboration.
• ▶ 10:52 The team's next major goal is computing the Busy Beaver value for six-rule Turing machines, known as BB(6).
• ▶ 11:00 Adding just one extra rule makes the problem dramatically harder, with nearly 60 quadrillion possible six-rule machines.
• ▶ 11:12 One particularly stubborn machine's halting behavior is connected to the Collatz conjecture, leading to doubt at ▶ 11:22 that BB(6) will ever be solved — though past doubts about BB(5) offer cautious hope.

• ▶ 0:01 The Busy Beaver Problem and the Origin of the Game (0:01 - 2:22) - Introduces the game, Turing machines, and Tibor Radó's 1962 formulation.
• ▶ 2:22 Halting, Rules, and Early Busy Beaver Values (2:22 - 6:35) - Explains halting, the game's rules, and the known BB(1) through BB(4) values.
• ▶ 6:35 The BB(5) Challenge and Hunt (6:35 - 8:18) - Covers Stérin's challenge and the BB(5) search history up to Marxen & Buntrock.
• ▶ 8:18 BB(5) Proof, Verification, and Collaboration (8:18 - 10:52) - Details deciders, manual holdout proofs, mxdys's verification, and community collaboration.
• ▶ 10:52 The Next Challenge: BB(6) (10:52 - 11:37) - Looks ahead to the team's next target, the Busy Beaver value for six rules.