2024/08/27/bb-2-4-proven

[utterances-bot]

S(2,4) = 3932964 | sligocki

We now know definitively that

https://www.sligocki.com//2024/08/27/bb-2-4-proven.html

[nickdrozd]

Cool result! Generally speaking colors are more powerful than states, so I was curious whether there would be any tricky ones in the 2-4 space.

If you are taking audience requests, could you do an updated post on the CTL method? I've read your previous post many times, but I still don't quite understand it (at least not well enough to implement). There were several open questions in that post too, and I assume the technique is better understood now. General regex, etc.

[sligocki]

If you are taking audience requests, could you do an updated post on the CTL method? I've read your previous post many times, but I still don't quite understand it (at least not well enough to implement). There were several open questions in that post too, and I assume the technique is better understood now. General regex, etc.

Yeah, we really need an update on CTL! Soooo much has happened since I wrote that post. One of the biggest problems is that I don't feel that I understand many of the improvements at a level I'd like before writing about them! That said, I think there's so much to say about this, it would be good to get some of it off of Discord, out of our brains and into posts!

[nickdrozd]

I checked the two holdouts you listed, and my simulator marks them both as infinite. But my simulator is not mathematically rigorous and is occasionally prone to false positives, which is very bad for formal proofs! For 1RB3LA1LA1RA_2LB2RA---0RB, my simulator takes 26602 cycles to get there (corresponding to 5599218 machine steps).

Both of the holdouts totally foil my backward reasoner (I think you call it "backtracking filter"). It's not just impossible for this method to show that they can't halt -- it's also impossible to show that they don't spin out and impossible to show that they don't blank the tape. I call these "unreasonable" programs.