[CaptainNegative]

Only finitely many values of BB can be mathematically determined. Once your Turing Machines become expressive enough to encode your (presumably consistent) proof system, they can begin encoding nonsense of the form "I will halt only after I manage to derive a proof that I won't ever halt", which means that their halting status (and the corresponding Busy Beaver value) fundamentally cannot be proven.

[karmakurtisaani]

Once you can express Collatz conjecture, you're already in the deep end.

[jerf]

Yes, but as far as I know, nobody has shown that the Collatz conjecture is anything other than a really hard problem. It isn't terribly difficult to mathematically imagine that perhaps the Collatz problem space considered generally encodes Turing complete computations in some mathematically meaningful way (even when we don't explicitly construct them to be "computational"), but as far as I know that is complete conjecture. I have to imagine some non-trivial mathematical time has been spent on that conjecture, too, so that is itself a hard problem.

But there is also definitely a place where your axiom systems become self-referential in the Busy Beaver and that is a qualitative change on its own. Aaronson and some of his students have put an upper bound on it, but the only question is exactly how loose it is, rather than whether or not it is loose. The upper bound is in the hundreds, but at [1] in the 2nd-to-last paragraph Scott Aaronson expresses his opinion that the true boundary could be as low as 7, 8, or 9, rather than hundreds.

[1]: https://scottaaronson.blog/?p=8972

[adgjlsfhk1]

https://people.cs.uchicago.edu/~simon/RES/collatz.pdf Generalized colatz is uncomputable.

[Veserv]

The bound on that is known to be no more than BB(745) which is independent of ZFC [1].

[1] https://scottaaronson.blog/?p=7388

[Kranar]

That's a misinterpretation of what the article says. There is no actual bound in principle to what can be computed. There is a fairly practical bound which is likely BB(10) for all intents and purposes, but in principle there is no finite value of n for which BB(n) is somehow mathematically unknowable.

ZFC is not some God given axiomatic system, it just happens to be one that mathematicians in a very niche domain have settled on because almost all problems under investigation can be captured by it. Most working mathematicians don't really concern themselves with it one way or another, almost no mathematical proofs actually reference ZFC, and with respect to busy beavers, it's not at all uncommon to extend ZFC with even more powerful axioms such as large cardinality axioms in order to investigate them.

Anyhow, just want to dispel a common misconception that comes up that somehow there is a limit in principle to what the largest BB(n) is that can be computed. There are practical limits for sure, but there is no limit in principle.

[IsTom]

You can compute a number that is equal to BB(n), but you can't prove that it is the right number you are looking for. For any fixed set of axioms you'll eventually run into BB(n) too big that gets indepentent.

[Kranar]

>You can compute a number that is equal to BB(n), but you can't prove that it is the right number you are looking for.

You can't categorically declare that something is unprovable. You can simply state that within some formal theory a proposition is independent, but you can't state that a proposition is independent of all possibly formal theories.

[tromp]

They didn't claim that. They claimed that any (sound and consistent) finitely axiomatizable theory (basically, any recursively enumerable set of theorems) can only prove finitely many theorems of the form BB(n) = N.

[Kranar]

I quoted the specific statement that I refuted.

[IsTom]

It's not that there "exists n, such that for all theories", but that "for all theories there exists n", that BB(n) will get independent eventually.