Coq-BB5

Apr 2024 · mxdys

Dependencies:

busycoq

FAR

Skelet #1 is a translated cycler – Coq agrees

MITMWFAR

n-GRAM CPS

Skelet #17 does not halt

Decider Formal Verification Coq Verifier Project

Featured Links

Github	https://github.com/ccz181078/Coq-BB5
Chat about it	https://discord.com/channels/960643023006490684/1218877181321678928
Forum Link	https://discuss.bbchallenge.org/t/proving-bb-5-in-coq/225

Description

In the initial release, Coq-BB5 was solving all machines but Skelet-17, it was added [shortly after](https://cosearch.bbchallenge.org/contribution/rcrq61n8) thus achieving the Coq proof of BB(5) = 47,176,870 https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237