Coq-BB5: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
m (coq -> rocq)
(link rocq to wikipedia)
 
(2 intermediate revisions by the same user not shown)
Line 1: Line 1:
{{Stub}}
{{Stub}}
Coq-BB5 is a Rocq 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.


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.

Latest revision as of 09:17, 25 August 2025

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.

See: https://github.com/ccz181078/Coq-BB5/tree/main

TODO: Give wiki links to these deciders and individual TM proofs.