Automated theorem proving by halting problem reduction Updated +Created
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".
Busy beaver function Updated +Created
is the largest number of 1's written by a halting -state Turing machine on a tape initially filled with 0's.
Video 1.
The Boundary of Computation by Mutual Information (2023)
Source.
Busy beaver scale Updated +Created
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 , we would be able to prove those conjectures automatically, by letting the machine run up to , and if it hadn't halted by then, we would know that it would never halt.
Of course, in practice, 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
Primitive recursive function Updated +Created
In intuitive terms it consists of all integer functions, possibly with multiple input arguments, that can be written only with a sequence of:
  • variable assignments
  • addition and subtraction
  • integer comparisons and if/else
  • for loops
for (i = 0; i < n; i++)
and such that n does not change inside the loop body, i.e. no while loops with arbitrary conditions.
n does not have to be a constant, it may come from previous calculations. But it must not change inside the loop body.
Primitive recursive functions basically include every integer function that comes up in practice. Primitive recursive functions can have huge complexity, and it strictly contains EXPTIME. As such, they mostly only come up in foundation of mathematics contexts.
The cool thing about primitive recursive functions is that the number of iterations is always bound, so we are certain that they terminate and are therefore computable.
This also means that there are necessarily functions which are not primitive recursive, as we know that there must exist uncomputable functions, e.g. the busy beaver function.
Adding unbounded while loops of course enables us to simulate arbitrary Turing machines, and therefore increases the complexity class.
More finely, there are non-primitive total recursive functions, e.g. most famously the Ackermann function.
R (complexity) Updated +Created
Set of all decision problems solvable by a Turing machine, i.e. that decide if a string belongs to a recursive language.
Recursively enumerable language Updated +Created
There is a Turing machine that halts for every member of the language with the answer yes, but does not necessarily halt for non-members.
The beauty of mathematics Updated +Created
Ciro Santilli intends to move his beauty list here little by little: github.com/cirosantilli/mathematics/blob/master/beauty.md
The most beautiful things in mathematics are results that are:
Good lists of such problems Lists of mathematical problems.
Whenever Ciro Santilli learns a bit of mathematics, he always wonders to himself:
Am I achieving insight, or am I just memorizing definitions?
Unfortunately, due to how man books are written, it is not really possible to reach insight without first doing a bit of memorization. The better the book, the more insight is spread out, and less you have to learn before reaching each insight.
Turing complete Updated +Created
A computer model that is as powerful as the most powerful computer model we have: Turing machine!
Turing machine decider Updated +Created
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
Turing machine regex tape notation Updated +Created
Turing machine regex tape notation is Ciro Santilli's made up name for the notation used e.g. at:Most of it is just regular regular expression notation, with a few differences:
  • denotes the right or left edge of the (zero initialized) tape. It is often omitted as we always just assume it is always present on both sides of every regex
  • A, B, C, D and E denotes the current machine state. This is especially common notation in the context of the BB(5) problem
  • < and > next to the state indicate if the head is on top of the left or right element. E.g.:
    11 (01)^n <A 00 (0011)^{n+2}
    indicates that the head A is on top of the last 1 of the last sequence of n 01s to the left of the head.
This notation is very useful, as it helps compress long repeated sequences of Turing machine tape and extract higher level patterns from them, which is how you go about understanding a Turing machin in order to apply Turing machine acceleration.
Undecidability requires infinitely many inputs Updated +Created
If there are infinitely many inputs, we can always construct a (potentially exponentially huge) Turing machine that hardcodes the outcome for every possible input, so the problem is never undecidable.
The problem is of course deciding and proving the outcome for each possible input, notably as it is possible that calculation for some of the inputs may be independent from ZFC.
Undecidable problem Updated +Created
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.
Coolest ones besides the obvious boring halting problem: