| Creator
|
Link
|
Notes
|
| bbchallenge
|
https://github.com/bbchallenge/bbchallenge-deciders
|
Official bbchallenge deciders
|
| @mxdys
|
https://github.com/ccz181078/Coq-BB5
|
Coq proof of BB(5) = 47,176,870. See Coq-BB5.
|
| @mei
|
https://github.com/meithecatte/busycoq
|
A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
|
| Georgi Georgiev (Skelet)
|
https://skelet.ludost.net/bb/
|
See bbfind and Skelet's 43 holdouts
Wrapped via bbfind-stdin by @wizord
|
| Mateusz Naściszewski @Mateon1
|
https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c
|
Accelerated TM simulators in Python utilizing memoization (like HashLife)
|
| Mateusz Naściszewski @Mateon1
|
https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b
|
Forward segment TM decider by @Mateon1 (variant of Halting Segment)
|
| Mateusz Naściszewski @Mateon1
|
https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc
|
Closed Position Set (CPS) TM decider implementation
|
| Mateusz Naściszewski @Mateon1
|
https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3
|
Closed Tape Language (CTL) SAT Solver; TODO dependencies still Discord posts
|
| @savask
|
https://github.com/savask/turing
|
Collection of deciders
|
| @savask
|
https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f
|
Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program
|
| @savask
|
https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72
|
Decider for Bouncers
|
| @savask
|
https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697
|
Reproduction of @mxdys' RepWL_ES decider (repeated block decider)
|
| @djmati1111
|
https://github.com/colette-b/bbchallenge
|
The first SAT-based Finite Automata Reduction (FAR) decider
|
| Frans Faase
|
https://github.com/FransFaase/SymbolicTM
|
An early Closed Tape Language (CTL) verifier
|
| @Iijil
|
https://github.com/Iijil1/Bouncers
|
Decider for Bouncers
|
| @Iijil
|
https://github.com/Iijil1/Bruteforce-CTL
|
Bruteforce Closed Tape Language (CTL) decider
|
| @Iijil
|
https://github.com/Iijil1/MITMWFAR
|
Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider
|
| @Iijil
|
https://gist.github.com/Iijil1/d325da33be74a86ac2399c161a57166a
|
4-symbol to 2-symbol TM compiler
|
| Jason Yuen
@-d
|
https://github.com/int-y1/proofs/tree/master/BusyLean
|
Some progress toward a FAR verifier checked by Lean
|
| Matthew House
@LegionMammal976
|
https://github.com/LegionMammal978/bigfoot-sim
|
An accelerated Bigfoot simulator
|
| Nathan Fenner
@nathanf
|
https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders
|
Formally verified deciders using Dafny
|
| Nathan Fenner
@nathanf
|
https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier
|
Formally verified Closed Tape Language (CTL) verifier
|
| Nathan Fenner
@nathanf
|
https://github.com/Nathan-Fenner/bbchallenge-regexy-decider
|
Closed Tape Language (CTL) decider
|
| Nathan Fenner
@nathanf
|
https://github.com/Nathan-Fenner/bb-simple-n-gram-cps
|
Dramatic Closed Position Set (CPS) simplification (much less resource-intensive and not as strong)
|
| @nickdrozd
|
https://github.com/nickdrozd/busy-beaver-stuff
|
|
| @start
|
https://github.com/phinanix/busy-beavers
|
|
| Shawn Ligocki
@sligocki
|
https://github.com/sligocki/busy-beaver
|
|
| Tony Guilfoyle
|
https://github.com/TonyGuil/bbchallenge
|
|
| Justin Blanchard
@UncombedCoconut
|
https://github.com/uncombedcoconut/bbchallenge
|
|
| Justin Blanchard
@UncombedCoconut
|
https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction
|
Finite Automata Reducion (FAR) decider
|
| Justin Blanchard
@UncombedCoconut
|
https://github.com/UncombedCoconut/bbchallenge-nfa-verification
|
Finite Automata Reducion (FAR) verifier
|
| Pavel Kropitz
@uni
|
https://github.com/univerz/bbc
|
|
| Dan Briggs
|
https://github.com/danbriggs/Turing
|
TM proofs/writing
|