Length of proof / machine for proving it can be much bigger than BB(n) itself. Or even there can be specific machines that don't halt, but there is no proof for

Length of proof / machine for proving it can be much bigger than BB(n) itself. Or even there can be specific machines that don't halt, but there is no proof for this at all – you can encode problems independent of ZFC in a few hundred states.