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.
If the website is defunct, statements by Scott Aaronson, peer reviewed papers, or other methods may be used to resolve the question if needed.
This is a near- duplicate of /BoltonBailey/will-the-5state-busy-beaver-be-know but for a later close date.
As of question writing, there are 2833 officially undecided machines, with a Coq proof not yet officially accepted that claims to prove all but 1 machine (Skelet's #17).
🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ731 | |
| 2 | Ṁ442 | |
| 3 | Ṁ227 | |
| 4 | Ṁ144 | |
| 5 | Ṁ54 |
https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237
We are extremely happy to announce that, after two years of intense collaboration, the goal of the Busy Beaver Challenge 4 has been reached: the conjecture “BB(5) 1 = 47,176,870” is proved.
Is this satisfying the resolution criterion?
https://wiki.bbchallenge.org/wiki/Main_Page
Notably, as part of bbchallenge.org, in June 2024 the 5th busy beaver value BB(5) was proven in Coq to be equal to the lower bound found in 1989[5]: 47,176,870.
Thanks, this is an exciting update! I'll dig into it a little more later.
My initial thought is that I copied the resolution text from the original market and now regret that decision; this description should be a lot clearer.
In particular, the "as determined by some page" part is a far looser criteria than I'd like; this isn't the official announcement, and the official count remains at 2833 undecided machines. The latest major update news post says they still don't have a process in place for accepting Coq proofs (which this is). So two pages on the site contradict each other.
I'd love to have other @traders weigh in.
This could be interesting. Here they talk about the release timeline of the BB(5) result: https://docs.google.com/document/u/0/d/16Glpzb92fDCrhYRgM_i6wnSIV82P8NNJDj8wvMRPqIU/mobilebasic#heading=h.sei53bybk10r
It's scheduled for July 2nd. All undecided machines will be marked as decided.
So you are more interested in the question "Will all BB(5) candidate machines have explicit deciders by EOY 2024?" rather than the original question?
I'm interested in the question "do we know the answer to some strong standard of proof". I think the original question mixes up several different standards: announcement on the main page of bbchallenge.org is a very different standard than a single page on their very sparse wiki, especially when the latest announcement explains that they aren't using the standard the wiki page in question is using.
I think "peer reviewed paper" is much closer to the "main announcement" standard than the "random wiki page" one. The difference between those two is literally a peer review process. It's mainly a peer review process targeting the question of "how do we handly Coq proofs", not "this specific Coq proof", but it's still such a process. I suspect "Scott Aaronson announces it" to be closer to the "peer reviewed" standard.
In particular, a claim of a Coq proof could still be faulty. There's discussion on the discord verifying that other people have been able to compile the proof. The setup / problem statement might not actually be right (even if the proof that follows is correct).
The wiki only appeared this week. I think in analogy it's closer to a preprint server. I think the original context of the question implied "formally announced by the bbchallenge project (assuming it's not defunct)", but that's not what was actually written, and now it's a mess.
The lazy answer is: looks like we'll have all ambiguity removed by July 2nd; wait till then and then resolve. And I could do that and just try to learn from the mistake and write the next question better, but I think it's a good exercise to figure out whether we should or shouldn't resolve this question, as written, now.
(Also, I'll refrain from trading on this question from now until at least some time after coming up with a decision re: this topic.)