Congrats!

[tcosmo]

This is really cool work, congrats!

You may be interested in formalising the result we had that there is a 15-state Turing machine encoding Erdõs's conjecture on powers of 2:

• Conjecture: "For all n > 8, the base-3 representation of 2^n contains a digit 2", https://www.erdosproblems.com/406
• Turing machine: https://dna.hamilton.ie/tsterin/bbsim/, powers_of_two_15_2.txt
• Paper explaining our construction: https://arxiv.org/abs/2107.12475

This is of course only a suggestion if you were interested!

Congrats again on your work,

Sincerely yours

[lengyijun]

I have read your paper and I think your Turing machine is undoubtedly correct.
No one doubts it and there seems no need to verify it.

[tcosmo]

Thank you! We have had reviews that the proof for the 2-symbol machine was obscure / hard to follow :(
But I agree that there is very little doubt!

Thank you again,

[tcosmo]

In a slightly related fashion but again in a case where there is little doubt, it could be interesting to formalising that Antihydra (1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA) halts if and only if answer to the following question is "YES":

Iterate Collatz-like function starting from 8:

- 3x/2 if even
- (3x-1)/2 if odd

Do you ever get twice as many more odd terms than even ones?

The main interest of having the formalisation would be to directly cite it in the in-preparation BB5 paper (which will end with discussions on BB6's hardness) rather than having to prove the equivalence in the paper (that is already going to be quite crowded).

A relatively formal analysis is given on the wiki. and on Shawn Ligocki's blog.

Of course I'm only sharing thoughts and feel free to completely ignore :)

I will stop "spamming" this issue now!

Thank you again,

EDIT: mxdys (Coq-BB5 author) pointed out that there're 5 known Antihydra-like cryptd in bb6, and all of them except Antihydra have Coq-proved rules:

https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra2.v
https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC.v
https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---.v
https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB.v

[lengyijun]

I think they can verify Antihydra in 10 min.
It seems that I don't need to participate.

[tcosmo]

I think they can verify Antihydra in 10 min. It seems that I don't need to participate.

I get the understanding that they are not going to do it as they are concentrating on making progress at deciding 6-state machines, and I think they would especially not do it in the way of showing its equivalent to the statement I mentioned (the proofs listed above "only" show a first step which is to show the abstract rules the machine is applying but then you would have to show that the rules correspond to the statement).

However, I fully understand your sentiment and of course won't insist if you are not interested!