We are extremely happy to officially release the results of [Decider] Bouncers, after a long but thorough validation process. The decider for bouncers is formally described and proved correct in Section 7 of bbchallenge’s official write-up. Many thanks to @TonyG who initially proposed the method and to all the contributors who participated to the consequent team effort that led to today’s release!
Intuitively, a bouncer is a Turing machine that populates a tape with linearly-expanding patterns, called repeaters, possibly separated or enclosed by fixed patterns called walls. Bouncers correspond to a wide range of behaviors, as illustrated by machines: #80,747,967, #88,427,177, #5,228,688 or #5,608,043.
Official 2,833 holdouts. The method decided 29,799 machines (91%) over the 32,632 that were left undecided after the previous release, in less than 2 seconds on a standard laptop using @meithecatte’s implementation. We are left with 2,833 machines to decide! Find these 2,833 machines on our undecided index repository. The certificates (i.e. data that is enough to prove that a machine is a bouncer) are available here.
Coq’s taking over. Formal verification of bbchallenge’s results is an ambitious goal that we were only dreaming of until contributors @meithecatte and @mxdys made very concrete steps in that direction using the Coq theorem prover:
-
busycoq, a pipeline for formally verifying certificates for bouncers (and for other bbchallenge deciders) in Coq was built by @meithecatte. This work also includes Coq proofs for Skelet’s machine #1, which is an insanely big translated cycler, and other notoriously hard undecided 5-state Turing machines.
-
coq-bb5, by @mxdys, which claims to prove the theorem
BB(5) = 47,176,870in Coq up to only one notoriously hard machine, Skelet’s machine #17, whose nonhalting is taken as an axiom. Deciding this machine has been attacked by @chxu, no Coq proof for it has been proposed yet.
These extremely promising Coq results are not yet officially released as part of bbchallenge as we need to define and apply a validation process for Coq proofs, similarly to what we have done for deciders. Hence, the machines decided in Coq, such as Skelet’s 1 are still marked undecided for now.
Nonetheless, bbchallenge’s endgame approaches and we’re very excited for what comes next!
Beaverly yours,
