Coq-BB5
Coq-BB5 is a Rocq (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the bbchallenge.org community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of BusyCoq maintained by meithecatte.
The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 (proof), Finned #2 (proof), Finned #3 (proof), Finned #4 (proof) and Finned #5 (proof)) and Skelet machines 1 (proof), 10 (proof), 15 (proof), 26 (proof), 33 (proof), 34 (proof) and 35 (proof).[1] Coq-BB5 imports these proofs from BusyCoq. The individual proof for non-halting of Skelet 17 (proof)(description) is contained within Coq-BB5 itself.[2]
See: https://github.com/ccz181078/Coq-BB5/tree/main
TODO: Give wiki links to these deciders and individual TM proofs.