Coq-BB5: Difference between revisions
Added Category:BB(5) |
Attempted to expand this a bit: Described locations of proofs for individual TMs |
||
| Line 1: | Line 1: | ||
{{Stub}} | {{Stub}} | ||
'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq 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. | '''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq 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 (#1, #2, [[Finned 3|#3]], #4, #5) and Skelet machines [[Skelet 1|1]], [[Skelet 10|10]], 15, 26, 33, 34 and 35.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> The individual proof for non-halting of [[Skelet 17]] is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref> | |||
See: https://github.com/ccz181078/Coq-BB5/tree/main | See: https://github.com/ccz181078/Coq-BB5/tree/main | ||
TODO: Give wiki links to these deciders and individual TM proofs. | TODO: Give wiki links to these deciders and individual TM proofs. | ||
== References == | |||
[[Category:BB(5)]] | [[Category:BB(5)]] | ||
Revision as of 19:02, 21 February 2026
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 (#1, #2, #3, #4, #5) and Skelet machines 1, 10, 15, 26, 33, 34 and 35.[1] The individual proof for non-halting of Skelet 17 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.