| 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. Wrapped via bbfind-stdin by @wizord
|
| @mxdys
|
Link
|
Coq proof of some deciders and some solved machines in BB(6)
|
| 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
|