Code repositories: Difference between revisions

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

Revision as of 11:14, 16 June 2024

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 Dramatic Closed Position Set (CPS) simplification (much less resource-intensive and not as strong)
@nickdrozd Link
@start 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
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=Code_repositories&oldid=216"