Code repositories
| Creator | Link | Notes |
|---|---|---|
| bbchallenge | Link | Official bbchallenge deciders |
| @mxdys | Link | Coq proof of BB(5) = 47,176,870. See Coq-BB5. |
| @mei | Link | A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs |
| Georgi Georgiev (Skelet) | Link | See bbfind and Skelet's 43 holdouts
Wrapped via bbfind-stdin by @wizord |
| Mateusz Naściszewski @Mateon1 | Link | Accelerated TM simulators in Python utilizing memoization (like HashLife) |
| Mateusz Naściszewski @Mateon1 | Link | Forward segment TM decider by @Mateon1 (variant of Halting Segment) |
| Mateusz Naściszewski @Mateon1 | Link | Closed Position Set (CPS) TM decider implementation |
| Mateusz Naściszewski @Mateon1 | Link | Closed Tape Language (CTL) SAT Solver;
TODO dependencies still Discord posts |
| @savask | Link | Collection of deciders |
| @savask | Link | Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program |
| @savask | Link | Decider for Bouncers |
| @savask | Link | Reproduction of @mxdys' RepWL_ES decider (repeated block decider) |
| @djmati1111 | Link | The first SAT-based Finite Automata Reduction (FAR) decider |
| Frans Faase | Link | An early Closed Tape Language (CTL) verifier |
| @Iijil | Link | Decider for Bouncers |
| @Iijil | Link | Bruteforce Closed Tape Language (CTL) decider |
| @Iijil | Link | Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider |
| @Iijil | Link | 4-symbol to 2-symbol TM compiler |
| Jason Yuen
@-d |
Link | Some progress toward a FAR verifier checked by Lean |
| Matthew House
@LegionMammal976 |
Link | An accelerated Bigfoot simulator |
| Nathan Fenner
@nathanf |
Link | Formally verified deciders using Dafny |
| Nathan Fenner
@nathanf |
Link | Formally verified Closed Tape Language (CTL) verifier |
| Nathan Fenner
@nathanf |
Link | Closed Tape Language (CTL) decider |
| Nathan Fenner
@nathanf |
Link | Closed Position Set (CPS) simplification: uses less resources and is less strong |
| @nickdrozd | Link | |
| @star | Link | |
| Shawn Ligocki
@sligocki |
Link | |
| Tony Guilfoyle | Link | |
| Justin Blanchard
@UncombedCoconut |
Link | |
| Justin Blanchard
@UncombedCoconut |
Link | Finite Automata Reducion (FAR) decider |
| Justin Blanchard
@UncombedCoconut |
Link | Finite Automata Reducion (FAR) verifier |
| Pavel Kropitz
@uni |
Link | |
| Dan Briggs | Link | TM proofs/writing |