Busy beaver

The busy beaver game consists in finding, for a given $n$, the turing machine with $n$ states that writes the largest possible number of 1's on a tape initially filled with 0's. In other words, computing the busy beaver function for a given $n$.

There are only finitely many Turing machines with $n$ states, so we are certain that there exists such a maxium. Computing the Busy beaver function for a given $n$ then comes down to solving the halting problem for every single machine with $n$ states.

Some variant definitions define it as the number of time steps taken by the machine instead. Wikipedia talks about their relationship, but no patience right now.

The Busy Beaver problem is cool because it puts the halting problem in a more precise numerical light, e.g.:

Bibliography:

The step busy beaver is a variant of the busy beaver game counts the number of steps before halt, instead of the number of 1's written to the tape.

As of 2023, it appears that BB(5) the same machine, , will win both for 5 states. But this is not always necessarily the case.

$BB(n)$ is the largest number of 1's written by a halting $n$-state Turing machine on a tape initially filled with 0's.

The following things come to mind when you look into research in this area, especially the search for BB(5) which was hard but doable:

Bibliography:

Turing machine acceleration refers to using high level understanding of specific properties of specific Turing machines to be able to simulate them much fatser than naively running the simulation as usual.

Acceleration allows one to use simulation to find infinite loops that might be very long, and would not be otherwise spotted without acceleration.

This is for example the case of www.sligocki.com/2023/03/13/skelet-1-infinite.html proof of Skelet machine #1.

Project trying to compute BB(5) once and for all. Notably it has better presentation and organization than any other previous effort, and appears to have grouped everyone who cares about the topic as of the early 2020s.

Very cool initiative!

By 2023, they had basically decided every machine: discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141

In June 2024 they felt that they had verified the result after a full Coq proof was published: So now onto BB(6) I guess.

The last value we will likely every know for the busy beaver function! BB(6) is likely completely out of reach forever.

By 2023, it had basically been decided by the The Busy Beaver Challenge as mentioned at: discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141, pending only further verification. It is going to be one of those highly computational proofs that will be needed to be formally verified for people to finally settle.

As that project beautifully puts it, as of 2023 prior to full resolution, this can be considered the:on the Busy beaver scale.

Best busy beaver machine known since 1989 as of 2023, before a full proof of all 5 state machines had been carried out.

Entry on The Busy Beaver Challenge: bbchallenge.org/1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA

Paper extracted to HTML by Heiner Marxen: turbotm.de/~heiner/BB/mabu90.html

List on The Busy Beaver Challenge: bbchallenge.org/skelet

Bibliography:

On The Busy Beaver Challenge: bbchallenge.org/68329601

Non formal proof with a program March 2023: www.sligocki.com/2023/03/13/skelet-1-infinite.html Awesome article that describes the proof procedure.

Formal proof August 2023: discuss.bbchallenge.org/t/skelet-1-is-a-translated-cycler-coq-agrees/166

The proof uses Turing machine acceleration to show that Skelet machine #1 is a Translated cycler Turing machine with humongous cycle paramters:

wiki.bbchallenge.org/wiki/Antihydra:

Also posted at:

The Busy beaver scale allows us to gauge the difficulty of proving certain (yet unproven!) mathematical conjectures!

To to this, people have reduced certain mathematical problems to deciding the halting problem of a specific Turing machine.

A good example is perhaps the Goldbach's conjecture. We just make a Turing machine that successively checks for each even number of it is a sum of two primes by naively looping down and trying every possible pair. Let the machine halt if the check fails. So this machine halts iff the Goldbach's conjecture is false! See also Conjecture reduction to a halting problem.

Therefore, if we were able to compute $BB(n)$, we would be able to prove those conjectures automatically, by letting the machine run up to $BB(n)$, and if it hadn't halted by then, we would know that it would never halt.

Of course, in practice, $BB$ is generally uncomputable, so we will never know it. And furthermore, even if it were computable, it would take a lot longer than the age of the universe to compute any of it, so it would be useless.

However, philosophically speaking at least, the number of states of the equivalent Turing machine gives us a philosophical idea of the complexity of the problem.

The busy beaver scale is likely mostly useless, since we are able to prove that many non-trivial Turing machines do halt, often by reducing problems to simpler known cases. But still, it is cute.

But maybe, just maybe, reduction to Turing machine form could be useful. E.g. The Busy Beaver Challenge and other attempts to solve BB(5) have come up with large number of automated (usually parametrized up to a certain threshold) Turing machine decider programs that automatically determine if certain (often large numbers of) Turing machines run forever.

So it it not impossible that after some reduction to a standard Turing machine form, some conjecture just gets automatically brute-forced by one of the deciders, this is a path to

If you can reduce a mathematical problem to the Halting problem of a specific turing machine, as in the case of a few machines of the Busy beaver scale, then using Turing machine deciders could serve as a method of automated theorem proving.

That feels like it could be an elegant proof method, as you reduce your problem to one of the most well studied representations that exists: a Turing machine.

However it also appears that certain problems cannot be reduced to a halting problem... OMG life sucks (or is awesome?): Section "Turing machine that halts if and only if Collatz conjecture is false".

bbchallenge.org/story#what-is-known-about-bb lists some (all?) cool examples,

wiki.bbchallenge.org/wiki/Cryptids contains a larger list. In June 2024 it was discovered that BB(6) is hard.

mathoverflow.net/questions/309044/is-there-a-known-turing-machine-which-halts-if-and-only-if-the-collatz-conjectur suggests one does not exist. Amazing.

Intuitively we see that the situation is fundamentally different from the Turing machine that halts if and only if the Goldbach conjecture is false because for Collatz the counter example must go off into infinity, while in Goldbach conjecture we can finitely check any failures.

Amazing.