Low Busy Beaver numbers can be computed. But at some point we must become unable to determine further BB numbers, since the function is an uncomputable function. (Assuming the physical Church-Turing thesis is true.)
We can get lower bounds on this crossover point by computing low numbers; we know up to BB(4), with some promising progress made on 5. And we can get upper bounds as well; for example Adam Yedidia built a 7918 state Turing machine whose behavior is independent of ZFC. Can we ever know the exact value of the crossover point? A BB(n) such that BB(n) can be known with certainty, but BB(n+1) cannot.
For "can be known with certainty", I'll for now use the definition "we know a specific algorithm that prints the number in binary and then halts". This definition is open to revision as needed.
This market resolves to YES if it's proven possible, and to NO if it's proven impossible. It resolves N/A if it's proven that we can't have such a proof, and if none of those are provable, it stays open forever.
I think you need to specify a (set of) allowed proof system(s). The answer might be different for ZF, ZFC, and ZFC + large cardinal properties, for example. And I think you can rank the large cardinals based on which BB values they prove, in the opposite direction of this approach:
From https://www.scottaaronson.com/papers/bb.pdf, pg 6.
So, is this market about a specific proof system? Or about the existence of any proof system with the specified property?
@IsaacKing Huh. That seems like an uninteresting answer.
The study of the busy beaver function is basically precisely the study of what weird shit happens and what edge cases pop up when you extremely carefully collide "real world" with "math" and see what settles from the debris. It is almost pathologically aimed at making a mess of questions like this market.
The outcome I expect from a market like this is that there are a pile of machines that halt, where we can describe the behavior of well enough to answer the question of "how long does it run" with high fidelity. The answers will be awkwardly huge exponential towers or worse things, and despite having a closed form answer there will be difficulty with stuff like "what's the first digit?".
And then there will be another pile of machines where we say "this weird axiom says it never halts". And as n gets larger, that pile and its axioms will get weirder and harder to understand, while the halting pile just gets large and unwieldy. And meanwhile anything having to do with BB(6) or higher is clearly not present in the Real World, because we're short a few atoms. But it will continue to look intuitively like there is a ground truth of the matter if you could "just" run it "long enough" to "see" what the answer is.
And that's what makes the problem fun to poke at. Because it breaks your intuitions and hurts your brain, but in a kinda-weird-kinda-good way. And definitely in a way that is aimed directly at breaking this question and ones like it.