Title: Amateurs Solve a Famous Computer Science Problem On Discord
Author: Quanta Magazine

Transcript:
There's a simple game played
with just two numbers, one and zero,
which after only a few rounds
becomes mind-bogglingly complex.
One of the things that's cool about this
problem is its depth,
it's a fun game to play.
It's a puzzle that asks this
about a computer program.
What's the longest,
most-complicated thing it can do,
and then stop?
It's called the Busy Beaver problem.
It's a busy beaver in the sense
that it's doing so many operations
and at some point it stops.
This simple game is connected
to some of the thorniest questions
in math and computer science.
Just as hard as the
hardest open problems in mathematics.
But recently, a motley group of amateurs
came together online
to tackle the toughest version
of the problem to date.
It's like candy for me or something,
people nerding out about this thing.
They ended up solving
this long-standing open question
faster than anyone thought possible.
Kind of a brave and slightly crazy
thing to do.
So how is the Busy Beaver game played?
And what was the secret
to the team's success?
The Busy Beaver game was formulated
by the Hungarian mathematician
Tibor Radó in 1962.
Radó was exploring the behavior
of theoretical computational devices
called Turing machines.
One of the simplest, formal models
of a universal computer.
Turing machines were conceived
in the 1930's
by the mathematician Alan Turing.
All Turing machines
contain three components.
An infinite tape that stores data
in cells as ones or zeros.
A head that reads the tape, writes a new number onto it,
and moves the tape left or right.
And a set of instructions, or
program, that tell the machine
exactly what to do at each step.
Turing machines are capable
of computing
anything that is computable
by algorithms.
By doing this very simple
but sort of esoteric
set of instructions,
you can do just as much as
you could do
with any other programing language.
A Turing machine's program
can have any number of rules
as summarized in a table.
This table contains one row
for each rule,
and two columns.
One for when the head reads a 'zero'.
And the other for when
the head encounters a 'one.'
Each rule tells the machine
what to write,
which way to move the tape,
and what rule to follow next.
All computer programs either
perform their function
and eventually stop,
known as halting,.
Or they get stuck in infinite
loops and run forever.
Useful programs are
programs that stop.
Here is an example of a two-rule
Turing machine that halts.
At the onset, all cells on the tape
are set to zero.
And it's set to follow rule A.
The head reads the tape and encounters a zero.
The machine then looks up the
rule in the zero column.
The instructions say to:
Write the number one.
Move one cell to the right.
The next rule to follow is rule B.
After writing the number one,
the machine then moves the
tape a cell to the right
The halting problem is at the heart
of the Busy Beaver game.
and encounters another zero.
The zero column in rule B
instructs the machine to:
Write a number one.
Move one cell to the left.
The next rule to follow is rule A
The Turing machine moves
the tape a cell to the left,
and this time encounters the one.
The rule A instructions in the one column
tell it to halt.
Here is a two-rule Turing machine
with different instructions,
which will cause it to never stop.
It quickly gets stuck in an endless loop.
Computer scientists want to know:
given the rules of a Turing machine,
is there a guaranteed way to tell
whether that machine will halt
or run forever?
This question is known
as the 'halting problem,'
and it can be extremely
hard to solve.
In some ways, what we're doing
we're trying to solve a little subsection
of the halting problem,
take a bite out of it.
The Busy Beaver game works like this.
First pick specific number of rules for your Turing machines
denoted 'N.'
This number determines
how many Turing machines
will exist in the group,
where each machine
has one distinct set of rules.
For example, with only one rule,
there are 25 Turing machines
each with a unique program.
However, many of them will do
the exact same thing.
With two rules. here are over 6000 distinct machines.
And for 'N' equals three,
or machines with three rules,
there are millions.
Now feed a tape of zeros into
each machine in the group
and see what happens next.
Some will halt quickly.
Others will run much longer,
while still others will keep
going and going forever.
For each value of 'N,'
there must be
one hard-working machine
that runs the longest
and then stops.
This is the 'Busy Beaver.'
The number of steps that the
Busy Beaver with
'N' rules takes before
halting is denoted BB(N).
The goal of the Busy Beaver
game is to identify
the Busy Beaver for a given group,
and determine how long it runs,
before halting.
For the group of one-rule
machines,
BB(1) is easy to determine
because there are essentially
only two outcomes.
If the rule tells the Turing
machine to halt
when it encounters a zero,
it will stop on the very first step.
Turing machines with
any other set of rules
will keep moving down
the tape of zeros forever.
This means that the solution
to BB(1) is one step.
The Busy Beaver value for
a two-rule Turing machine
is six steps.
For BB(3), the longest-running
machine that still halts
runs for 21 steps.
But when you get to BB(4)
things start to get more interesting.
Now you're getting Turing
machines that can
start to do pretty-complicated things.
With four rules, there are billions of Turing machines
to sort through and evaluate.
And for some of these machines,
the halting problem is
fiendishly difficult.
To many, BB(4) seemed unsolvable.
But in 1974, computer scientist, Allen Brady,
finally succeeded.
He determined that the Busy
Beaver for a
four-rule Turing machine runs for 107 steps.
For decades, BB(4) looked
like the end of the road.
But then a French graduate student
named Tristan Stérin entered the picture.
After reading an article by
computer scientist Scott Aaronson,
Stérin got hooked on BB(5).
It felt hard enough, but not too hard,
it's what you want in an open problem.
So in 2022, Stérin created
a website
dedicated to solving BB(5)
and named the endeavor
the Busy Beaver Challenge.
We have to create a tool so that people
can start working on the problems,
so it's less overwhelming, it's
not just one person,
it's more distributed.
Word soon gone out about
the challenge,
and people from all over the
world joined in.
The hope was to build
a little scientific community.
But with five rules,
there are nearly 17 trillion
possible Turing machines.
Where do you even begin
the search?
The hunt for BB(5) has
a long history.
In 1983, nearly 100 people gathered
in the West German city of Dortmund
for a competition to find BB(5),
but ultimately they all fell short.
However, two Busy Beaver hunters,
graduate students Heiner Marxen
and Jürgen Buntrock,
continued the hunt.
With a powerful new computer,
they identified a possible contender,
which halted after a staggering 47,176,870 steps.
The pair conjectured that this was,
in fact, the fifth Busy Beaver,
but they couldn't prove it.
Marxen and Buntrock's
five-rule contender
gave the Busy Beaver
challengers a starting point.
Now the team needed to devise methods
to prove that no machine exists
that runs longer
than this contender and still halts.
The first step was to
construct a database
of five-state Turing machines
with the property that,
they are the only machines
you need to consider.
Stérin wrote a computer program
that winnowed the list of
trillions of machines
down to 88 million.
All the rest were either redundant
or halted before Marxen
and Buntrock's machine.
In phase two, it was to invite people
to write programs that we call 'deciders.'
These deciders analyze machines
to determine whether they
will eventually halt
or run forever.
A sufficiently good new
decider might eliminate
90 to 99% of the remaining
unsolved machines,
so it's a huge impact.
To verify the accuracy of these deciders,
the decentralized group of
around 20 challengers,
some of them anonymous,
devised a validation system.
Someone else has to reproduce
your results independently,
and then you have to write in
a formal mathematical way.
Using deciders, the group
reduced the list of contenders
to around 30 holdouts
which couldn't be cracked
with computers
requiring a different approach.
Attack each of these one off
and try to prove, you know,
manually that this specific
machine never halts.
Over the following months,
the team communicated
through Discord forums
and posted their progress
to the BB Challenge website.
We would be getting updates about
like, we're down to 15.
We're down to six machines,
you know.
And eventually, like, you know, it got down to one,
which was one of the hardest
ones to prove.
Finally, they had tentative proofs
for all machines.
What remained was the arduous
work of verifying everything.
But then in April of 2024,
a mysterious new contributor
known only by a pseudonym
joined in to finish the job
Somebody with the handle 'mxdys'
showed up on the forum
and basically said like, hey,
I have written a Coq proof,
Using a computer-assisted proof
verification system called Coq,
'mxdys' swiftly completed
the challenge.
In about one month or two,
had formalized everything we
had done and more
to come to a final solution.
It turns out that the contender
identified by Marxen and Buntrock
30 years earlier, which halted after 47 million steps,
was the fifth busy beaver after all.
Now we have the
computer-verified proof
and we are working on the
human-readable proof.
The way that this happened
was because
of the collaboration in the community,
sharing their ideas, bouncing
those off of other people,
it couldn't happen without it.
Meanwhile, part of the team
has moved on to new endeavors.
The most straightforward one is, well,
can we find the six-state champion?
However, with the addition of
just one rule,
the Busy Beaver problem
becomes much, much harder.
There are nearly 60 quadrillion
possible six-rule Turing machines.
One specific machine
is especially vexing.
The question of whether it halts
resembles a famously intractable math problem
called the Collatz conjecture.
Maybe six is something which
no group of human beings,
no matter how crazy and obsessed
and dedicated they are,
will ever calculate.
Currently, it seems that it's
quite impossible to solve BB(6),
but people said that for BB(5).