Code repositories: Difference between revisions
Jump to navigation
Jump to search
m (Fix typos) |
m (update ctl links) |
||
| Line 49: | Line 49: | ||
|[https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 Link] | |[https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 Link] | ||
|Python 3 | |Python 3 | ||
|[[Closed Tape Language | |[[Closed Tape Language]] SAT Solver; '''TODO dependencies still Discord posts''' | ||
|- | |- | ||
|@savask | |@savask | ||
| Line 79: | Line 79: | ||
|[https://github.com/FransFaase/SymbolicTM Link] | |[https://github.com/FransFaase/SymbolicTM Link] | ||
|C++ | |C++ | ||
|An early [[Closed Tape Language | |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 | |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 | |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 | |[[Closed Tape Language]] decider | ||
|- | |- | ||
|Nathan Fenner @nathanf | |Nathan Fenner @nathanf | ||
Revision as of 07:10, 25 August 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 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 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 (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 |