Nevertheless, we clearly do have some finite amount of information about this sequence, evident in the axioms of PA or ZFC or any other formal system that proves an infinite number of programs as non-halting (hence why the Busy Beaver project has been able to provably confirm BB(5)). We presume these systems are truly consistent and sound even if that fact is itself unprovable, so then where exactly did the non-halting information in the axioms of these systems “come from”?
Levin stops short of speculating about that, simply leaving it at the fact that what we have so far cannot be extended further by either algorithmic or random means. But if that’s the case, then either AI is capped at these same predictive limits as well (i.e., in the sense of problems AI could solve that humans could not, both given unlimited resources), or there is additional non-halting information embedded in the environment that an AI could “extract” better than a human. (I suppose it’s also possible we haven’t fully exploited the non-halting information we do have, but I think that’s unlikely since we’re not even sure whether BB(6) is ZFC-provable and that’s a rather tiny machine).