Code repositories: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
m (Tighten up the table a bit.) |
||
| Line 19: | Line 19: | ||
|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]] | |See [[bbfind]] and [[Skelet's 43 holdouts]]. Wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord] | ||
Wrapped via | |||
|- | |- | ||
|Mateusz Naściszewski @Mateon1 | |Mateusz Naściszewski @Mateon1 | ||
| Line 36: | Line 35: | ||
|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; | |[[Closed Tape Language (CTL)]] SAT Solver; '''TODO dependencies still Discord posts''' | ||
'''TODO dependencies still Discord posts''' | |||
|- | |- | ||
|@savask | |@savask | ||
| Line 79: | Line 77: | ||
|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] | ||
|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] | ||
|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] | ||
|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] | ||
|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] | ||
|[[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 and is less strong | |[[Closed Position Set (CPS)]] simplification: uses less resources and is less strong | ||
| Line 117: | Line 109: | ||
| | | | ||
|- | |- | ||
|Shawn Ligocki | |Shawn Ligocki @sligocki | ||
@sligocki | |||
|[https://github.com/sligocki/busy-beaver Link] | |[https://github.com/sligocki/busy-beaver Link] | ||
| | | | ||
| Line 126: | Line 117: | ||
| | | | ||
|- | |- | ||
|Justin Blanchard | |Justin Blanchard @UncombedCoconut | ||
@UncombedCoconut | |||
|[https://github.com/uncombedcoconut/bbchallenge Link] | |[https://github.com/uncombedcoconut/bbchallenge Link] | ||
| | | | ||
|- | |- | ||
|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 | |[[Finite Automata Reducion (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 | |[[Finite Automata Reducion (FAR)]] verifier | ||
|- | |- | ||
|Pavel Kropitz | |Pavel Kropitz @uni | ||
@uni | |||
|[https://github.com/univerz/bbc Link] | |[https://github.com/univerz/bbc Link] | ||
| | | | ||
Revision as of 10:49, 24 November 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 | Closed Position Set (CPS) simplification: uses less resources and is less strong |
| @nickdrozd | Link | |
| @star | 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 |