Coq-BB5 - Revision history

Polygon: /* Deciders */ description of halt-decider

2026-04-03T10:55:35Z

Deciders: description of halt-decider

← Older revision		Revision as of 10:55, 3 April 2026
Line 7:		Line 7:

	== Deciders ==		== Deciders ==
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v], simulates machines for a fixed number of steps, only checks for halting.
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated cycler\|Lin recurrence]].		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated cycler\|Lin recurrence]].

Polygon: /* Deciders */ linked to the correct page directly instead of via a redirect

2026-04-02T14:43:48Z

Deciders: linked to the correct page directly instead of via a redirect

← Older revision		Revision as of 14:43, 2 April 2026
Line 9:		Line 9:
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated ~~Cycler~~\|Lin recurrence]].		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated cycler\|Lin recurrence]].
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.

Polygon: Linked deciders

2026-04-02T14:34:59Z

Linked deciders

← Older revision		Revision as of 14:34, 2 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].		'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many [[deciders]] and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].

	== Individual proofs ==		== Individual proofs ==

Polygon: /* Deciders */ description of Loop.v

2026-04-02T14:34:29Z

Deciders: description of Loop.v

← Older revision		Revision as of 14:34, 2 April 2026
Line 9:		Line 9:
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v], this decider simulates TMs for a fixed number of steps, checking for halting and [[Translated Cycler\|Lin recurrence]].
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.

Polygon: /* Deciders */ augmentations

2026-04-02T14:28:18Z

Deciders: augmentations

← Older revision		Revision as of 14:28, 2 April 2026
Line 10:		Line 10:
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v]		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v]
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], ~~see~~ [[NGram CPS]] ~~for details on how this decider works~~.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], Coq-BB5 uses regular [[NGram CPS]] aswell as the Fixed-length history and Least Recent Usage history (LRU) augmentations.
	* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.		* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.

Polygon: /* Deciders */ listed deciders

2026-04-02T14:24:46Z

Deciders: listed deciders

← Older revision		Revision as of 14:24, 2 April 2026
Line 7:		Line 7:

	== Deciders ==		== Deciders ==
			* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt.v Halt.v]
			* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Halt_BB5.v Halt_BB5.v]
			* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_Loop.v Loop.v]
			* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_NGramCPS.v NGramCPS.v], see [[NGram CPS]] for details on how this decider works.
			* [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/Deciders/Decider_RepWL.v RepWL.v], see [[Repeated Word List]] for details.

	See: https://github.com/ccz181078/Coq-BB5/tree/main		See: https://github.com/ccz181078/Coq-BB5/tree/main

Polygon: Some structuring

2026-04-02T14:19:03Z

Some structuring

← Older revision		Revision as of 14:19, 2 April 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].		'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].

			== Individual proofs ==

	The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), [[Skelet 26#Skelet 15\|15]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), [[Skelet 26\|26]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), [[Skelet 33\|33]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>		The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), [[Skelet 26#Skelet 15\|15]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), [[Skelet 26\|26]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), [[Skelet 33\|33]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>

			== Deciders ==

	See: https://github.com/ccz181078/Coq-BB5/tree/main		See: https://github.com/ccz181078/Coq-BB5/tree/main

Polygon: Linked Skelet 15 and Skelet 26

2026-03-07T18:28:34Z

Linked Skelet 15 and Skelet 26

← Older revision		Revision as of 18:28, 7 March 2026
Line 2:		Line 2:
	'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].		'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].

	The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), [[Skelet 33\|33]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>		The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), [[Skelet 26#Skelet 15\|15]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), [[Skelet 26\|26]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), [[Skelet 33\|33]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>

	See: https://github.com/ccz181078/Coq-BB5/tree/main		See: https://github.com/ccz181078/Coq-BB5/tree/main

Polygon: Linked Skelet 33

2026-03-02T17:32:18Z

Linked Skelet 33

← Older revision		Revision as of 17:32, 2 March 2026
Line 2:		Line 2:
	'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].		'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].

	The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), 33 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>		The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), [[Skelet 33\|33]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>

	See: https://github.com/ccz181078/Coq-BB5/tree/main		See: https://github.com/ccz181078/Coq-BB5/tree/main

Polygon: Added other domains that were proven

2026-02-21T19:29:02Z

Added other domains that were proven

← Older revision		Revision as of 19:29, 21 February 2026
Line 1:		Line 1:
	{{Stub}}		{{Stub}}
	'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte.		'''Coq-BB5''' is a [https://en.wikipedia.org/wiki/Rocq Rocq] (previously known as Coq) proof that BB(5) = 47,176,870. It combines many deciders and individual TM proofs that the [[bbchallenge.org]] community developed and described over the years 2022-2024. It is maintained by mxdys and includes a snapshot of [[BusyCoq]] maintained by meithecatte. Coq-BB5 also contains proofs of the values of [[BB(2)]], [[BB(3)]], [[BB(4)]], [[BB(2,3)]] and [[BB(2,4)]].

	The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), 33 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>		The individual TM proofs are - except for Skelet 17 - all contained within the included snapshot of BusyCoq. TMs which have individual proofs in BusyCoq are: The "finned" machines (Finned #1 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned1.v proof]), Finned #2 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned2.v proof]), [[Finned 3\|Finned #3]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned3.v proof]), Finned #4 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned4.v proof]) and Finned #5 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Finned5.v proof])) and Skelet machines [[Skelet 1\|1]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet1.v proof]), [[Skelet 10\|10]] ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet10.v proof]), 15 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet15.v proof]), 26 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet26.v proof]), 33 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet33.v proof]), 34 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet34.v proof]) and 35 ([https://github.com/ccz181078/Coq-BB5/blob/main/BusyCoq/Skelet35.v proof]).<ref>https://github.com/ccz181078/Coq-BB5/tree/main/BusyCoq</ref> Coq-BB5 [https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Sporadic_Machines.v imports] these proofs from BusyCoq. The individual proof of non-halting for [[Skelet 17]] ([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v proof])([https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.md description]) is contained within Coq-BB5 itself.<ref>https://github.com/ccz181078/Coq-BB5/tree/main/CoqBB5/BB5/Deciders</ref>