Code repositories - Revision history

Int-y1 at 07:40, 14 February 2026

2026-02-14T07:40:56Z

← Older revision		Revision as of 07:40, 14 February 2026
Line 109:		Line 109:
	\|[https://github.com/int-y1/busy-beaver-cpp Link]		\|[https://github.com/int-y1/busy-beaver-cpp Link]
	\|C++		\|C++
	\|C++ version of Quick_Sim.py		\|C++ version of Shawn Ligocki's Quick_Sim.py
	\|-		\|-
	\|Matthew House @LegionMammal976		\|Matthew House @LegionMammal976

Int-y1: add C++ Quick_Sim.py

2026-02-14T07:39:54Z

add C++ Quick_Sim.py

← Older revision		Revision as of 07:39, 14 February 2026
Line 105:		Line 105:
	\|Lean 4		\|Lean 4
	\|Some progress toward a FAR verifier checked by Lean		\|Some progress toward a FAR verifier checked by Lean
			\|-
			\|Jason Yuen @-d
			\|[https://github.com/int-y1/busy-beaver-cpp Link]
			\|C++
			\|C++ version of Quick_Sim.py
	\|-		\|-
	\|Matthew House @LegionMammal976		\|Matthew House @LegionMammal976

Int-y1: coq -> rocq

2025-08-25T09:04:10Z

coq -> rocq

← Older revision		Revision as of 09:04, 25 August 2025
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

Int-y1: update far link

2025-08-25T08:34:59Z

update far link

← Older revision		Revision as of 08:34, 25 August 2025
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
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

Int-y1: edit cps link

2025-08-25T08:28:13Z

edit cps link

← Older revision		Revision as of 08:28, 25 August 2025
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
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 129:		Line 129:
	\|[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

Int-y1: update ctl links

2025-08-25T07:10:28Z

update ctl links

← Older revision		Revision as of 07:10, 25 August 2025
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 ~~(CTL)~~]] SAT Solver; '''TODO dependencies still Discord posts'''		\|[[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 ~~(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

Sligocki: Fix typos

2025-07-22T18:37:42Z

Fix typos

← Older revision		Revision as of 18:37, 22 July 2025
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 ~~Reducion~~ (FAR)]] decider		\|[[Finite Automata Reduction (FAR)]] 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 ~~Reducion~~ (FAR)]] verifier		\|[[Finite Automata Reduction (FAR)]] verifier
	\|-		\|-
	\|Pavel Kropitz @uni		\|Pavel Kropitz @uni

Int-y1: make table sortable

2025-07-09T02:58:13Z

make table sortable

← Older revision		Revision as of 02:58, 9 July 2025
Line 1:		Line 1:
	{\| class="wikitable"		{\| class="wikitable sortable"
	\|+		\|+
	!Creator		!Creator

Int-y1: add a lean 4 repo

2025-07-07T08:53:41Z

add a lean 4 repo

← Older revision		Revision as of 08:53, 7 July 2025
Line 175:		Line 175:
	\|Java		\|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		\|@mxdys

Int-y1: add languages

2025-07-07T05:46:50Z

add languages

Show changes