BusyBeaver(6) Is Quite Large

It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.

What makes BB(748) independent of ZFC is not its value, but the fact that one of the 748-state machines (call it TM_ZFC_INC) looks for an inconsistency (proof of FALSE) in ZFC and only halts upon finding one.

Thus, any proof that BB(748) = N must either show that TM_ZF_INC halts within N steps or never halts. By Gödel's famous results, neither of those cases is possible if ZFC is assumed to be consistent.

I think what's most unintuitive is that most (all?) "paradoxes" or "unknowables" in mathematics involve infinities. When limiting ourselves to finite whole numbers, paradoxes necessarily disappear.

BB(748) is by definition a finite number, and it has some value - we just don't know what it is. If an oracle told us the number, and we ran TM_ZFC_INC that many steps we would know for sure whether ZFC was consistent or not based on whether it terminated.

The execution of the turing machine can be encoded in ZFC, so it really is the value of BB(748) that is the magic ingredient. Somehow even knowledge of the value of this finite number is a more potent axiomatic system than any we've developed.

BB(748) is a finite number, but I'd argue its magic also comes from infinites: the fact some Turing Machines run forever and never halt.

Is it? If it's not possible to prove that it's the best solution to bb(748), does it even exist in any meaningful way?

I'm not sure what you mean. First of all BB(n) is a function so it has value(s).

And in theory we can prove BB(748)=X, where X is a plain big natural number, as long as we just assume ZFC is consistent. It's practically impossible, but not fundamentally impossible like proving Con(ZFC) in ZFC itself.