Proof of #34, #35 and possibly #33, #26 & #15

[sligocki]

Hi Dan, it's great to see a fellow BB hunter :) I thought you might be interested to see that I recently published a proof of Skelet #34 and a follow-up post sketching out how I think this can be generalized to #35, #33, #26 & #15. The last three are pretty hand-wavy at the moment, but I think the proofs can be tightened up with a little bit of elbow grease! Let me know if you have any questions.

[danbriggs]

Wow, thanks so much for your message! It looks like great work, and I'll try to read it in detail.

I looked back at my paper, and I guess I realized that 34 and 35 were nearly the same, and 33 was very similar to them. And I see from the beginning of my readme that I noticed that about 26 as well. But I didn't notice the similarity of machine 15, even though I put quite a bit of effort into it.

I've also seen this webpage bbchallenge.org because of your story. Over the past year I have been thinking about trying to formalize the proof of BB4 S & Σ in Coq or Lean together with my friend Harold @hrldcpr. After that we could start extending the library to deal with the more difficult BB5. It would be interesting to find out what you and the people on the page think about that!

[sligocki]

Great to hear back so quickly!

I highly recommend you come join the bbchallenge.org Discord channel: https://discord.gg/3uqtPJA9Uv . It's a very active group of people working on new methods for trying to hammer out BB5 and we have often found ourselves referencing your results on Skelet's holdouts. It would be great to have you join and share your work!

I am very interested in formal proving of BB results. I have some experience with Coq, but have had slow going formalizing these proofs. But @Nathan-Fenner has had a lot of success formalizing proof for our deciders using Dafny (a formal proof system I had not heard of before): https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders . This sort of thing is also being discussed on the Discord.

[hrldcpr]

Since Dan tagged me, for the record here is the work I did in Lean a year ago—but it's for extremely trivial machines, so much more work would be needed to do anything meaningful— https://github.com/hrldcpr/lean-halting

[sligocki]

Ooh, thanks for sharing! I spent several months (years ago) trying to implement macro machines and tape compression in Coq to prove TMs infinite. I think there's a lot of potential here, but it's also tough. Every time I created a new abstraction, I had to re-prove everything, and (at least in Coq) that was not a smooth experience.

[hrldcpr]

Yeah I agree it would be tough. Though I do think Lean is a bit slicker than Coq, and even more importantly it has a very active community (at https://leanprover.zulipchat.com/). If some Lean experts there joined forces with bbchallenge.org I could imagine it leading to cool things.