Code repositories: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
m (Fix typos)
m (coq -> rocq)
 
(3 intermediate revisions by the same user not shown)
Line 14: Line 14:
|[https://github.com/ccz181078/Coq-BB5 Link]
|[https://github.com/ccz181078/Coq-BB5 Link]
|Rocq
|Rocq
|Coq proof of BB(5) = 47,176,870. See [[Coq-BB5]].
|Rocq 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?
|Rocq, Rust, OCaml?
|A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs
|A hybrid Rocq/Rust/OCaml repo implementing very fast deciders plus verified proofs
|-
|-
|Georgi Georgiev ([[Skelet]])
|Georgi Georgiev ([[Skelet]])
Line 29: Line 29:
|[https://github.com/ccz181078/busycoq/tree/BB6/verify Link]
|[https://github.com/ccz181078/busycoq/tree/BB6/verify Link]
|Rocq
|Rocq
|Coq proof of some deciders and some solved machines in BB(6)
|Rocq proof of some deciders and some solved machines in BB(6)
|-
|-
|Mateusz Naściszewski @Mateon1
|Mateusz Naściszewski @Mateon1
Line 44: Line 44:
|[https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Link]
|[https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Link]
|Python 3
|Python 3
|[[Closed Position Set (CPS)]] TM decider implementation
|[[Closed Position Set]] 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]
|Python 3
|Python 3
|[[Closed Tape Language (CTL)]] SAT Solver; '''TODO dependencies still Discord posts'''
|[[Closed Tape Language]] SAT Solver; '''TODO dependencies still Discord posts'''
|-
|-
|@savask
|@savask
Line 59: Line 59:
|[https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Link]
|[https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f Link]
|Haskell
|Haskell
|[[Closed Position Set (CPS)]], reverse-engineered from Skelet's [[bbfind]] program
|[[Closed Position Set]], reverse-engineered from Skelet's [[bbfind]] program
|-
|-
|@savask
|@savask
Line 74: Line 74:
|[https://github.com/colette-b/bbchallenge Link]
|[https://github.com/colette-b/bbchallenge Link]
|Python 3
|Python 3
|The first SAT-based [[Finite Automata Reduction (FAR)]] decider
|The first SAT-based [[Finite Automata Reduction]] decider
|-
|-
|Frans Faase
|Frans Faase
|[https://github.com/FransFaase/SymbolicTM Link]
|[https://github.com/FransFaase/SymbolicTM Link]
|C++
|C++
|An early [[Closed Tape Language (CTL)]] verifier
|An early [[Closed Tape Language]] verifier
|-
|-
|@Iijil
|@Iijil
Line 89: Line 89:
|[https://github.com/Iijil1/Bruteforce-CTL Link]
|[https://github.com/Iijil1/Bruteforce-CTL Link]
|Go
|Go
|Bruteforce [[Closed Tape Language (CTL)]] decider
|Bruteforce [[Closed Tape Language]] decider
|-
|-
|@Iijil
|@Iijil
Line 119: Line 119:
|[https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier Link]
|[https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier Link]
|Dafny
|Dafny
|Formally verified [[Closed Tape Language (CTL)]] verifier
|Formally verified [[Closed Tape Language]] verifier
|-
|-
|Nathan Fenner @nathanf
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/bbchallenge-regexy-decider Link]
|[https://github.com/Nathan-Fenner/bbchallenge-regexy-decider Link]
|Rust
|Rust
|[[Closed Tape Language (CTL)]] decider
|[[Closed Tape Language]] decider
|-
|-
|Nathan Fenner @nathanf
|Nathan Fenner @nathanf
|[https://github.com/Nathan-Fenner/bb-simple-n-gram-cps Link]
|[https://github.com/Nathan-Fenner/bb-simple-n-gram-cps Link]
|Rust
|Rust
|[[Closed Position Set (CPS)]] simplification: uses less resources and is less strong
|[[Closed Position Set]] simplification: uses less resources and is less strong
|-
|-
|@nickdrozd
|@nickdrozd
Line 159: Line 159:
|[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]
|Rust
|Rust
|[[Finite Automata Reduction (FAR)]] decider
|[[Finite Automata Reduction]] decider
|-
|-
|Justin Blanchard @UncombedCoconut
|Justin Blanchard @UncombedCoconut
|[https://github.com/UncombedCoconut/bbchallenge-nfa-verification Link]
|[https://github.com/UncombedCoconut/bbchallenge-nfa-verification Link]
|Python 3
|Python 3
|[[Finite Automata Reduction (FAR)]] verifier
|[[Finite Automata Reduction]] verifier
|-
|-
|Pavel Kropitz @uni
|Pavel Kropitz @uni

Latest revision as of 09:04, 25 August 2025

Creator Link Main language Notes
bbchallenge Link ? Official bbchallenge deciders
@mxdys Link Rocq Rocq proof of BB(5) = 47,176,870. See Coq-BB5.
@mei Link Rocq, Rust, OCaml? A hybrid Rocq/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 Rocq 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 TM decider implementation
Mateusz Naściszewski @Mateon1 Link Python 3 Closed Tape Language SAT Solver; TODO dependencies still Discord posts
@savask Link Haskell Collection of deciders
@savask Link Haskell Closed Position Set, 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 decider
Frans Faase Link C++ An early Closed Tape Language verifier
@Iijil Link Go Decider for Bouncers
@Iijil Link Go Bruteforce Closed Tape Language 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 verifier
Nathan Fenner @nathanf Link Rust Closed Tape Language decider
Nathan Fenner @nathanf Link Rust Closed Position Set 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 decider
Justin Blanchard @UncombedCoconut Link Python 3 Finite Automata Reduction 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=3358"