Code repositories: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
No edit summary
No edit summary
Line 14: Line 14:
|@mxdys
|@mxdys
|https://github.com/ccz181078/Coq-BB5
|https://github.com/ccz181078/Coq-BB5
|
|Coq proof of BB(5) = 47,176,870. See [[Coq-BB5]].
|-
|-
|@mei
|@mei
Line 25: Line 25:
Wrapped via  [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
Wrapped via  [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
|-
|-
|@Mateon1
|Mateusz Naściszewski @Mateon1
|https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c
|https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c
|Accelerated TM simulators in Python utilizing memoization (like HashLife)
|Accelerated TM simulators in Python utilizing memoization (like HashLife)
|-
|-
|@Mateon1
|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
|}
|}
* [https://github.com/bbchallenge/bbchallenge-deciders The official bbchallenge deciders repo]                                                       
*
* [https://github.com/ccz181078/Coq-BB5 Coq-BB5 by @mxdys]
* [https://github.com/meithecatte/busycoq A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei]         
* [https://skelet.ludost.net/bb/ bbfind by Skelet] wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
* [https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c Accelerated TM simulators in Python utilizing memoization (like HashLife), by @Mateon1]
* [https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b Forward segment TM decider by @Mateon1 (variant of Halting Segment)]
* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Closed Position Set (CPS) TM decider  by @Mateon1]
* [https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 SAT Solver CTL code by @Mateon1; TODO dependencies still in Discord posts]
* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program, by @savask]
* [https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Bouncers decider, by @savask]
* [https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Reproduction of mxdys' repeated blocks decider, by @savask]
* [https://github.com/savask/turing Collection of deciders by @savask]
* [https://github.com/colette-b/bbchallenge The first SAT-based CTL/FAR decider, by @djmati1111]
* [https://github.com/FransFaase/SymbolicTM An early CTL verifier (regex-based) by Frans Faase]
* [https://github.com/Iijil1/Bouncers Bouncers decider, by @Iijil]
* [https://github.com/Iijil1/Bruteforce-CTL Bruteforce-CTL decider, by @Iijil]
* [https://github.com/Iijil1/MITMWFAR Meet-in-the-Middle Weighted Finite Automata... Reduction... by @Iijil]
* https://gist.github.com/Iijil1/d325da33be74a86ac2399c161a57166a
* [https://github.com/int-y1/proofs/tree/master/BusyLean Some progress toward a FAR verifier checked by Lean, by @-d]
* [https://github.com/int-y1/proofs/tree/master/BusyLean Some progress toward a FAR verifier checked by Lean, by @-d]
* [https://github.com/LegionMammal978/bigfoot-sim An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978]   
* [https://github.com/LegionMammal978/bigfoot-sim An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978]   

Revision as of 11:01, 16 June 2024

Repositories of bbchallenge.org contributors

Deciders

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
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=Code_repositories&oldid=213"