Ciro Santilli @cirosantilli 34

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".

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:

$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 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

Given stuff like arxiv.org/pdf/2107.12475.pdf on Erdős' conjecture on powers of 2, it feels like this one will be somewhere close to computer science/Halting problem issues than number theory. Who knows. This is suggested e.g. at The Busy Beaver Competition: a historical survey by Pascal Michel.

Once you hear about the uncomputability of such problems, it makes you see that all Diophantine equation questions risk being undecidable, though in some simpler cases we manage to come up with answers. The feeling is similar to watching people trying to solve the Halting problem, e.g. in the effort to determine BB(5).

A Turing machine decider is a program that decides if one or more Turing machines halts of not.

Of course, because what we know about the halting problem, there cannot exist a single decider that decies all Turing machines.

E.g. The Busy Beaver Challenge has a set of deciders clearly published, which decide a large part of BB(5). Their proposed deciders are listed at: discuss.bbchallenge.org/c/deciders/5 and actually applied ones at: bbchallenge.org.

But there are deciders that can decide large classes of turing machines.

Many (all/most?) deciders are based on simulation of machines with arbitrary cutoff hyperparameters, e.g. the cutoff space/time of a Turing machine cycler decider.

The simplest and most obvious example is the Turing machine cycler decider

The prototypical example is the Busy beaver function, which is the easiest example to reach from the halting problem.

Is a decision problem of determining if something belongs to a non-recursive language.

Or in other words: there is no Turing machine that always halts for every input with the yes/no output.

Every undecidable problem must obviously have an infinite number of "possibilities of stuff you can try": if there is only a finite number, then you can brute-force it.

Some undecidable problems are of recursively enumerable language, e.g. the halting problem.

Lists of undecidable problems.

Coolest ones besides the obvious boring halting problem:

A Turing machine that simulates another Turing machine/input pair that has been encoded as a string.

In other words: an emulator!

The concept is fundamental to state several key results in computer science, notably the halting problem.