The Busy Beaver function BB(n) asks for the runtime of the Turing Machine with n states that runs for the longest time before halting. Currently, the values for n < 6 are known and BB(745) is known to be independent of ZFC (https://scottaaronson.blog/?p=8972, https://scottaaronson.blog/?p=7388), but the exact cutoff point is unknown.

I will resolve YES upon a proof that some specific Turing Machine is the Busy Beaver for n states, even if the number can't be written concisely, and NO upon a proof that a machine with n states is undecidable in ZFC. This proof would have to be in a stronger system. If there are doubts about the consistency of that system, I'll defer to mathematical consensus (current large cardinal axioms up to I0 are considered okay).

The BB community has established a norm of both formalizing its results in Rocq and writing them up (starting with BB(5)), so I will wait for such an announcement. I believe that this is objective enough for me to bet on this market, but I'll first wait a week in case any demands for clarifications come up.