This question resolves YES if the Busy Beaver Challenge has been completed by the close date, as determined by some page on the bbchallenge.org website indicating that all 5-state Turing Machines have been decided. An exception is that if all machines are decided, but the Busy Beaver is still not known (due to multiple machines being known to halt but it being unclear which runs longest), that will not be enough to resolve the market YES.
Close date updated to 2024-06-01 11:59 pm
Oct 3, 3:12pm: In the interest of keeping the title in line with the description in the scenario where the above website goes defunct, I'll add another possibility for YES resolution: If Scott Aaronson makes a public statement that the 5-state Busy Beaver is known, then I will accept that as a Yes.
Related questions
https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141/3
Of the 32632 remaining machines, @UncombedCoconut has undocumented code that produces easy to verify certificates for all but 34 of them. These certificates have been verified by multiple independent sources. The only reason why they are not counted as official is because there is not yet formal documentation of how to reproduce these certificates - otherwise, we can safely say that they’re counted.
Of the 34 remaining machines, 31 belong to specific categories. For most of these categories, there is a proof that at least one of the machines do not halt. To prove the remaining machines do not halt, copy the existing proofs nearly verbatim, with small modifications that have yet to be determined. It would be excellent to see writeups for every machine here:
[..]
The 3 remaining machines have all been proved non-halting, but again, these have to be checked!
[..]
@Mqrius It sounds like the proof hasn't actually been completed for 31 of the machines yet. Also, I'm not sure what this source is or what they mean by a "certificate", so it's possible that none of this is reliable to begin with.
@JosephNoonan The "certificates" are finite automata reductions of the machines. More details here: https://discuss.bbchallenge.org/t/decider-finite-automata-reduction/123
Finding the certificates is much harder than verifying them. But, once verified, it doesn't matter where the certificate comes from -- it's a proof for the machine in question (when coupled with the proven verification program).
BBChallenge isn't yet using those certificates in their official list of decided machines, but this is because they would like to be able to reproduce their generation to the same standards of transparency and reproducibility that they use for their verification. AIUI, the certificates are all verified by the same decider that they have accepted as proving a large number of other machines.
Note that the "holdouts" aren't necessarily undecided, or even undecided to the high standards of rigor demanded; they're just not decided by a program that decides a sufficiently large number of machines.
I believe the count for the 34 holdouts is actually:
31 categorized machines, in 6 categories. Of the 31 machines, 8 have been proven non-halting, with those 8 machines spanning 4 of the 6 categories.
3 uncategorized machines, all proven non-halting by individual proofs.
Leaving 20 machines undecided, but all with strong heuristic arguments that they do not halt.
So something could certainly go wrong in the verification process, and the strong heuristic arguments for the undecided holdout machines might not convert into proofs. Or the work simply might not be completed in the timeframe of this question.
But the above is the basis of my YES position.
Curious if it only counts if bbchallenge.org does it or if someone else does it if that would also count? Or like, as written, it only counts if that one website does it, but that seems a bit weird, so I'm pointing it out.
@SeraphinaNix Yeah, if it's 8unambiguously resolved by someone else it should presumably resolve to YES. That said, assuming the website isn't abandoned, it should update to the right conclusion even if the work gets published elsewhere.
@SeraphinaNix It's a bit tricky because someone might come out with an unverified preprint claiming a resolution and it might not get reviewed before the end date. To bring the title more in line with the description, I'll add that if Scott Aaronson says on his blog or somewhere that it's been completely solved, then I'll accept that as well.