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.
replies(12):
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 guess it's also hard when we have an arbitrary Turing machine and have to prove that what it's doing isn't equilavent to trying to prove an undecibable statement.