Nerd-sniped by a half cooked math hackernews comment, I spent a few hours writing and visualizing a busy beaver simulator. Anyways, the theory is much cooler.
It's a finite number that represents the maximum number of steps a Turing machine with n states can take before halting.
The Busy Beaver function is denoted as BB(n).
BB(1) = 1, BB(2) = 4, BB(3) = 6, BB(4) = 13, BB(5) = 47176870
BB(6) had an earlier lower bound of $10^{18267}$ which has since been updated to be far, far larger.
BB increases quick, in fact it grows faster than any computable function. Why?
Let's say there exists another computable function (F) which upper bounds BB. Which implies that for any turing machine with k states, you
can say that it will run for a maximum number of F(k) steps before halting. If it runs for more than that, you can conclude
that the machine must never halt.
This sounds an awful lot like a solution for the halting problem, which Turing proved to be undecidable in 1936. Proof by contradiction.
We'll actually never know. Not because it is too big, but because we simply cannot compute it even with infinite time and memory (it is a finite number!).
Some crazy people have actually brought the upper bound for the largest BB number we can compute down to just 747. Which means that we cannot ever compute BB(748).
A turing machine with 748 states doesn't sound like much at all - and here it is.
ZFC is the standard set of axioms that we base our mathematics on. It is a set of axioms that we believe to be consistent and can be used to prove all the theorems we have proven so far, and more.
What does it mean for a set of axioms to be consistent? - it means that using this set, we should never be able to prove both a statement and its negation (i.e. something that is both true and false at the same time).
Godel proved that if ZFC is in fact consistent, it will never be able to prove its own consistency. This is Godel's second incompleteness theorem.
Proof:
Now let's say we have a turing machine that takes the axioms present in ZFC and starts enumerating all the provable statements one by one. By Godel's theorem, ZFC can't prove if this machine will ever halt (as halting would imply ZFC proving its own consistency).
The authors managed to bring the number of states required to build such a turing machine down to just 748 - which means that if
via ZFC we ever could calculate BB(748), we could just run this machine for BB(748) number of steps and prove ZFC's consistency; a contradiction to Godel.
Hence, BB(748) must be a finite yet incalculable number.
:Endproof
It blows my mind that this is a finite number by definition, that we can never compute without disproving our entire mathematical foundation!
Feels almost poetically quantum - a measurable quantity that exists; but if we measure it, our math collapses.