Coq-BB5: Difference between revisions
No edit summary |
Added other domains that were proven |
||
| (7 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
{{Stub}} | {{Stub}} | ||
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. | '''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 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]]. | ||
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 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), 33 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) 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)]] | |||
Latest revision as of 19:29, 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. Coq-BB5 also contains proofs of the values of BB(2), BB(3), BB(4), BB(2,3) and BB(2,4).
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 of non-halting for 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.