Code repositories: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
(Created page with "This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them. * [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]...")
 
m (Fix typos)
 
(17 intermediate revisions by 6 users not shown)
Line 1: Line 1:
This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them.
{| class="wikitable sortable"
 
|+
* [https://github.com/bbchallenge/bbchallenge-deciders The official bbchallenge deciders repo]                                                       
!Creator
* [https://github.com/ccz181078/Coq-BB5 Coq-BB5 by @mxdys]
!Link
* [https://github.com/meithecatte/busycoq A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei]          
!Main language
* [https://skelet.ludost.net/bb/ bbfind by Skelet] wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
!Notes
* [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)]
|bbchallenge
* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Closed Position Set (CPS) TM decider by @Mateon1]
|[https://github.com/bbchallenge/bbchallenge-deciders Link]
* [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]
|Official bbchallenge deciders
* [https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Bouncers decider, by @savask]
|-
* [https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Reproduction of mxdys' repeated blocks decider, by @savask]
|@mxdys
* [https://github.com/colette-b/bbchallenge The first SAT-based CTL/FAR decider, by @djmati1111]
|[https://github.com/ccz181078/Coq-BB5 Link]
* [https://github.com/FransFaase/SymbolicTM An early CTL verifier (regex-based) by Frans Faase]
|Rocq
* [https://github.com/Iijil1/Bouncers Bouncers decider, by @Iijil]
|Coq proof of BB(5) = 47,176,870. See [[Coq-BB5]].
* [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]
|@mei
* [https://github.com/int-y1/proofs/tree/master/BusyLean Some progress toward a FAR verifier checked by Lean, by @-d]
|[https://github.com/meithecatte/busycoq Link]
* [https://github.com/LegionMammal978/bigfoot-sim An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978] 
|Rocq, Rust, OCaml?
* [https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders Deciders formally verified using Dafny, by @nathanf]
|A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
* [https://github.com/Nathan-Fenner/bbchallenge-regexy-decider CTL decider by @nathanf]
|-
* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps A dramatic simplification of CPS (much less resource-intensive and not as strong) by @nathanf]
|Georgi Georgiev ([[Skelet]])
* [https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier A formally verified CTL checker by @nathanf]
|[https://skelet.ludost.net/bb/ Link]
* https://github.com/nickdrozd/busy-beaver-stuff    
|Pascal
* https://github.com/phinanix/busy-beavers
|See [[bbfind]]. Wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
* https://github.com/sligocki/busy-beaver
|-
* https://github.com/TonyGuil/bbchallenge
|@mxdys
* https://github.com/uncombedcoconut/bbchallenge
|[https://github.com/ccz181078/busycoq/tree/BB6/verify Link]
* https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction
|Rocq
* https://github.com/UncombedCoconut/bbchallenge-nfa-verification
|Coq proof of some deciders and some solved machines in BB(6)
* https://github.com/univerz/bbc
|-
 
|Mateusz Naściszewski @Mateon1
* [https://github.com/danbriggs/Turing TM proofs/writing by Dan Briggs]
|[https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c Link]
|Python 3
|Accelerated TM simulators in Python utilizing memoization (like HashLife)
|-
|Mateusz Naściszewski @Mateon1
|[https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b Link]
|Python 3
|Forward segment TM decider by @Mateon1 (variant of [[Halting Segment]])
|-
|Mateusz Naściszewski @Mateon1
|[https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Link]
|Python 3
|[[Closed Position Set (CPS)]] TM decider implementation
|-
|Mateusz Naściszewski @Mateon1
|[https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 Link]
|Python 3
|[[Closed Tape Language (CTL)]] SAT Solver; '''TODO dependencies still Discord posts'''
|-
|@savask
|[https://github.com/savask/turing Link]
|Haskell
|Collection of deciders
|-
|@savask
|[https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Link]
|Haskell
|[[Closed Position Set (CPS)]], reverse-engineered from Skelet's [[bbfind]] program
|-
|@savask
|[https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Link]
|Haskell
|Decider for [[Bouncers]]
|-
|@savask
|[https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Link]
|Haskell
|Reproduction of @mxdys' [[RepWL_ES]] decider (repeated block decider)
|-
|@djmati1111
|[https://github.com/colette-b/bbchallenge Link]
|Python 3
|The first SAT-based [[Finite Automata Reduction (FAR)]] decider
|-
|Frans Faase
|[https://github.com/FransFaase/SymbolicTM Link]
|C++
|An early [[Closed Tape Language (CTL)]] verifier
|-
|@Iijil
|[https://github.com/Iijil1/Bouncers Link]
|Go
|Decider for [[Bouncers]]
|-
|@Iijil
|[https://github.com/Iijil1/Bruteforce-CTL Link]
|Go
|Bruteforce [[Closed Tape Language (CTL)]] decider
|-
|@Iijil
|[https://github.com/Iijil1/MITMWFAR Link]
|Go
|[[Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR)]] decider
|-
|@Iijil
|[https://gist.github.com/Iijil1/d325da33be74a86ac2399c161a57166a Link]
|PHP
|4-symbol to 2-symbol TM compiler
|-
|Jason Yuen @-d
|[https://github.com/int-y1/proofs/tree/master/BusyLean Link]
|Lean 4
|Some progress toward a FAR verifier checked by Lean
|-
|Matthew House @LegionMammal976
|[https://github.com/LegionMammal978/bigfoot-sim Link]
|Rust
|An accelerated [[Bigfoot]] simulator
|-
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders Link]
|Dafny, Rust?
|Formally verified deciders using Dafny
|-
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier Link]
|Dafny
|Formally verified [[Closed Tape Language (CTL)]] verifier
|-
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/bbchallenge-regexy-decider Link]
|Rust
|[[Closed Tape Language (CTL)]] decider
|-
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/bb-simple-n-gram-cps Link]
|Rust
|[[Closed Position Set (CPS)]] simplification: uses less resources and is less strong
|-
|@nickdrozd
|[https://github.com/nickdrozd/busy-beaver-stuff Link]
|?
|
|-
|@star
|[https://github.com/phinanix/busy-beavers Link]
|?
|
|-
|Shawn Ligocki @sligocki
|[https://github.com/sligocki/busy-beaver Link]
|Python 3, Rust, C++
|
|-
|Tony Guilfoyle
|[https://github.com/TonyGuil/bbchallenge Link]
|C++
|
|-
|Justin Blanchard @UncombedCoconut
|[https://github.com/uncombedcoconut/bbchallenge Link]
|Python 3
|
|-
|Justin Blanchard @UncombedCoconut
|[https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction Link]
|Rust
|[[Finite Automata Reduction (FAR)]] decider
|-
|Justin Blanchard @UncombedCoconut
|[https://github.com/UncombedCoconut/bbchallenge-nfa-verification Link]
|Python 3
|[[Finite Automata Reduction (FAR)]] verifier
|-
|Pavel Kropitz @uni
|[https://github.com/univerz/bbc Link]
|Rust
|
|-
|Dan Briggs
|[https://github.com/danbriggs/Turing Link]
|Java
|TM proofs/writing
|-
|Thomas Vigouroux @Vigoux
|[https://git.sr.ht/~vigoux/busybeaver/tree/master Link]
|Lean 4
|An attempt at formalising results regarding Busy Beavers. Contains deciders and their proof of correctness.
|-
|@mxdys
|[https://github.com/ccz181078/TM Link]
|C++
|Enumerating 7x2 TMs
|}

Latest revision as of 18:37, 22 July 2025

Creator Link Main language Notes
bbchallenge Link ? Official bbchallenge deciders
@mxdys Link Rocq Coq proof of BB(5) = 47,176,870. See Coq-BB5.
@mei Link Rocq, Rust, OCaml? A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
Georgi Georgiev (Skelet) Link Pascal See bbfind. Wrapped via bbfind-stdin by @wizord
@mxdys Link Rocq Coq proof of some deciders and some solved machines in BB(6)
Mateusz Naściszewski @Mateon1 Link Python 3 Accelerated TM simulators in Python utilizing memoization (like HashLife)
Mateusz Naściszewski @Mateon1 Link Python 3 Forward segment TM decider by @Mateon1 (variant of Halting Segment)
Mateusz Naściszewski @Mateon1 Link Python 3 Closed Position Set (CPS) TM decider implementation
Mateusz Naściszewski @Mateon1 Link Python 3 Closed Tape Language (CTL) SAT Solver; TODO dependencies still Discord posts
@savask Link Haskell Collection of deciders
@savask Link Haskell Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program
@savask Link Haskell Decider for Bouncers
@savask Link Haskell Reproduction of @mxdys' RepWL_ES decider (repeated block decider)
@djmati1111 Link Python 3 The first SAT-based Finite Automata Reduction (FAR) decider
Frans Faase Link C++ An early Closed Tape Language (CTL) verifier
@Iijil Link Go Decider for Bouncers
@Iijil Link Go Bruteforce Closed Tape Language (CTL) decider
@Iijil Link Go Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider
@Iijil Link PHP 4-symbol to 2-symbol TM compiler
Jason Yuen @-d Link Lean 4 Some progress toward a FAR verifier checked by Lean
Matthew House @LegionMammal976 Link Rust An accelerated Bigfoot simulator
Nathan Fenner @nathanf Link Dafny, Rust? Formally verified deciders using Dafny
Nathan Fenner @nathanf Link Dafny Formally verified Closed Tape Language (CTL) verifier
Nathan Fenner @nathanf Link Rust Closed Tape Language (CTL) decider
Nathan Fenner @nathanf Link Rust Closed Position Set (CPS) simplification: uses less resources and is less strong
@nickdrozd Link ?
@star Link ?
Shawn Ligocki @sligocki Link Python 3, Rust, C++
Tony Guilfoyle Link C++
Justin Blanchard @UncombedCoconut Link Python 3
Justin Blanchard @UncombedCoconut Link Rust Finite Automata Reduction (FAR) decider
Justin Blanchard @UncombedCoconut Link Python 3 Finite Automata Reduction (FAR) verifier
Pavel Kropitz @uni Link Rust
Dan Briggs Link Java TM proofs/writing
Thomas Vigouroux @Vigoux Link Lean 4 An attempt at formalising results regarding Busy Beavers. Contains deciders and their proof of correctness.
@mxdys Link C++ Enumerating 7x2 TMs
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=Code_repositories&oldid=2565"