Code repositories: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
No edit summary
m (Fix typos)
 
(9 intermediate revisions by 6 users not shown)
Line 1: Line 1:
{| class="wikitable"
{| class="wikitable sortable"
|+
|+
!Creator
!Creator
!Link
!Link
!Main language
!Notes
!Notes
|-
|-
|bbchallenge
|bbchallenge
|[https://github.com/bbchallenge/bbchallenge-deciders Link]
|[https://github.com/bbchallenge/bbchallenge-deciders Link]
|?
|Official bbchallenge deciders
|Official bbchallenge deciders
|-
|-
|@mxdys
|@mxdys
|[https://github.com/ccz181078/Coq-BB5 Link]
|[https://github.com/ccz181078/Coq-BB5 Link]
|Rocq
|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 Link]
|[https://github.com/meithecatte/busycoq Link]
|Rocq, Rust, OCaml?
|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/ Link]
|[https://skelet.ludost.net/bb/ Link]
|See [[bbfind]] and  [[Skelet's 43 holdouts]]
|Pascal
Wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
|See [[bbfind]]. Wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
|-
|@mxdys
|[https://github.com/ccz181078/busycoq/tree/BB6/verify Link]
|Rocq
|Coq proof of some deciders and some solved machines in BB(6)
|-
|-
|Mateusz Naściszewski @Mateon1
|Mateusz Naściszewski @Mateon1
|[https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c Link]
|[https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c Link]
|Python 3
|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 Link]
|[https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b Link]
|Python 3
|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 Link]
|[https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Link]
|Python 3
|[[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 Link]
|[https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 Link]
|[[Closed Tape Language (CTL)]] SAT Solver;  
|Python 3
'''TODO dependencies still Discord posts'''
|[[Closed Tape Language (CTL)]] SAT Solver; '''TODO dependencies still Discord posts'''
|-
|-
|@savask
|@savask
|[https://github.com/savask/turing Link]
|[https://github.com/savask/turing Link]
|Haskell
|Collection of deciders
|Collection of deciders
|-
|-
|@savask
|@savask
|[https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Link]
|[https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Link]
|Haskell
|[[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 Link]
|[https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Link]
|Haskell
|Decider for [[Bouncers]]
|Decider for [[Bouncers]]
|-
|-
|@savask
|@savask
|[https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Link]
|[https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Link]
|Haskell
|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 Link]
|[https://github.com/colette-b/bbchallenge Link]
|Python 3
|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 Link]
|[https://github.com/FransFaase/SymbolicTM Link]
|C++
|An early [[Closed Tape Language (CTL)]] verifier
|An early [[Closed Tape Language (CTL)]] verifier
|-
|-
|@Iijil
|@Iijil
|[https://github.com/Iijil1/Bouncers Link]
|[https://github.com/Iijil1/Bouncers Link]
|Go
|Decider for [[Bouncers]]
|Decider for [[Bouncers]]
|-
|-
|@Iijil
|@Iijil
|[https://github.com/Iijil1/Bruteforce-CTL Link]
|[https://github.com/Iijil1/Bruteforce-CTL Link]
|Go
|Bruteforce [[Closed Tape Language (CTL)]] decider
|Bruteforce [[Closed Tape Language (CTL)]] decider
|-
|-
|@Iijil
|@Iijil
|[https://github.com/Iijil1/MITMWFAR Link]
|[https://github.com/Iijil1/MITMWFAR Link]
|Go
|[[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 Link]
|[https://gist.github.com/Iijil1/d325da33be74a86ac2399c161a57166a Link]
|PHP
|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 Link]
|[https://github.com/int-y1/proofs/tree/master/BusyLean Link]
|Lean 4
|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 Link]
|[https://github.com/LegionMammal978/bigfoot-sim Link]
|Rust
|An accelerated [[Bigfoot]] simulator
|An accelerated [[Bigfoot]] simulator
|-
|-
|Nathan Fenner
|Nathan Fenner @nathanf
@nathanf
|[https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders Link]
|[https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders Link]
|Dafny, Rust?
|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 Link]
|[https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier Link]
|Dafny
|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 Link]
|[https://github.com/Nathan-Fenner/bbchallenge-regexy-decider Link]
|Rust
|[[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 Link]
|[https://github.com/Nathan-Fenner/bb-simple-n-gram-cps Link]
|[[Closed Position Set (CPS)]] simplification: uses less resources & is less strong
|Rust
|[[Closed Position Set (CPS)]] simplification: uses less resources and is less strong
|-
|-
|@nickdrozd
|@nickdrozd
|[https://github.com/nickdrozd/busy-beaver-stuff Link]
|[https://github.com/nickdrozd/busy-beaver-stuff Link]
|?
|
|
|-
|-
|@start
|@star
|[https://github.com/phinanix/busy-beavers Link]
|[https://github.com/phinanix/busy-beavers Link]
|?
|
|
|-
|-
|Shawn Ligocki
|Shawn Ligocki @sligocki
@sligocki
|[https://github.com/sligocki/busy-beaver Link]
|[https://github.com/sligocki/busy-beaver Link]
|Python 3, Rust, C++
|
|
|-
|-
|Tony Guilfoyle
|Tony Guilfoyle
|[https://github.com/TonyGuil/bbchallenge Link]
|[https://github.com/TonyGuil/bbchallenge Link]
|C++
|
|
|-
|-
|Justin Blanchard
|Justin Blanchard @UncombedCoconut
@UncombedCoconut
|[https://github.com/uncombedcoconut/bbchallenge Link]
|[https://github.com/uncombedcoconut/bbchallenge Link]
|Python 3
|
|
|-
|-
|Justin Blanchard
|Justin Blanchard @UncombedCoconut
@UncombedCoconut
|[https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction Link]
|[https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction Link]
|[[Finite Automata Reducion (FAR)]] decider
|Rust
|[[Finite Automata Reduction (FAR)]] decider
|-
|-
|Justin Blanchard
|Justin Blanchard @UncombedCoconut
@UncombedCoconut
|[https://github.com/UncombedCoconut/bbchallenge-nfa-verification Link]
|[https://github.com/UncombedCoconut/bbchallenge-nfa-verification Link]
|[[Finite Automata Reducion (FAR)]] verifier
|Python 3
|[[Finite Automata Reduction (FAR)]] verifier
|-
|-
|Pavel Kropitz
|Pavel Kropitz @uni
@uni
|[https://github.com/univerz/bbc Link]
|[https://github.com/univerz/bbc Link]
|Rust
|
|
|-
|-
|Dan Briggs
|Dan Briggs
|[https://github.com/danbriggs/Turing Link]
|[https://github.com/danbriggs/Turing Link]
|Java
|TM proofs/writing
|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"