In principle, you could reduce the problem into running a few very costly programs, so that the proof is completely verified as soon as someone eats that cost. (Some 6-state machines are already looking like they'll take a galactic cost to prove, and others will take a cost just barely within reason.) But this definitely isn't the case for the BB(5) project.