BusyBeaverWiki - User contributions [en]

File:BB6 holdouts 4521.txt

2024-11-04T17:22:34Z

UncombedCoconut: Sigh.

== Summary ==
Sigh.

Beaver Math Olympiad

2024-09-02T17:24:55Z

UncombedCoconut: Tweak English wording.

'''Beaver Mathematical Olympiad''' (BMO) is an attempt to re-formulate the halting problem for some particular Turing machines as a mathematical problem in a style suitable for a hypothetical math olympiad.

The purpose of the BMO is twofold. First, statements where non-essential details (related to tape encoding, number of steps, etc.) are discarded are more suitable to be shared with mathematicians who perhaps are able to help. Second, it's a way to jokingly highlight how a hard question could appear deceptively simple.

== Unsolved problems ==

=== 1. {{TM|1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE|undecided}} ===

Let <math>(a_n)_{n \ge 1}</math> and <math>(b_n)_{n \ge 1}</math> be two sequences such that <math>(a_1, b_1) = (1, 2)</math> and

<math display="block">(a_{n+1}, b_{n+1}) = \begin{cases}
(a_n-b_n, 4b_n+2) & \text{if }a_n \ge b_n \\
(2a_n+1, b_n-a_n) & \text{if }a_n < b_n
\end{cases}</math>

for all positive integers <math>n</math>. Does there exist a positive integer <math>i</math> such that <math>a_i = b_i</math>?

The first 10 values of <math>(a_n, b_n)</math> are <math>(1, 2), (3, 1), (2, 6), (5, 4), (1, 18), (3, 17), (7, 14), (15, 7), (8, 30), (17, 22)</math>.

=== 2. [[Hydra]] and [[Antihydra]] ===

Let <math>(a_n)_{n \ge 0}</math> be a sequence such that <math>a_{n+1} = a_n+\left\lfloor\frac{a_n}{2}\right\rfloor</math> for all non-negative integers <math>n</math>.

# If <math>a_0=3</math>, does there exist a non-negative integer <math>k</math> such that the list of numbers <math>a_0, a_1, a_2, \dots, a_k</math> have more than twice as many even numbers as odd numbers? ([[Hydra]])
# If <math>a_0=8</math>, does there exist a non-negative integer <math>k</math> such that the list of numbers <math>a_0, a_1, a_2, \dots, a_k</math> have more than twice as many odd numbers as even numbers? ([[Antihydra]])

=== 5. {{TM|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE|undecided}} ===

Let <math>(a_n)_{n \ge 1}</math> and <math>(b_n)_{n \ge 1}</math> be two sequences such that <math>(a_1, b_1) = (0, 5)</math> and

<math display="block">(a_{n+1}, b_{n+1}) = \begin{cases}
(a_n+1, b_n-f(a_n)) & \text{if } b_n \ge f(a_n) \\
(a_n, 3b_n+a_n+5) & \text{if } b_n < f(a_n)
\end{cases}</math>

where <math>f(x)=10\cdot 2^x-1</math>

for all positive integers <math>n</math>. Does there exist a positive integer <math>i</math> such that <math>b_i = f(a_i)-1</math>?

== Solved problems ==

=== 3. {{TM|1RB0RB3LA4LA2RA_2LB3RA---3RA4RB|non-halt}} and {{TM|1RB1RB3LA4LA2RA_2LB3RA---3RA4RB|non-halt}} ===

Let <math>v_2(n)</math> be the largest integer <math>k</math> such that <math>2^k</math> divides <math>n</math>. Let <math>(a_n)_{n \ge 0}</math> be a sequence such that

<math display="block">a_n = \begin{cases}
2 & \text{if } n=0 \\
a_{n-1}+2^{v_2(a_{n-1})+2}-1 & \text{if } n \ge 1
\end{cases}</math>

for all non-negative integers <math>n</math>. Is there an integer <math>n</math> such that <math>a_n=4^k</math> for some positive integer <math>k</math>?

Link to Discord discussion: https://discord.com/channels/960643023006490684/1084047886494470185/1252634913220591728

=== 4. {{TM|1RB3RB---1LB0LA_2LA4RA3LA4RB1LB|non-halt}} ===

Bonnie the beaver was bored, so she tried to construct a sequence of integers <math>\{a_n\}_{n \ge 0}</math>. She first defined <math>a_0=2</math>, then defined <math>a_{n+1}</math> depending on <math>a_n</math> and <math>n</math> using the following rules:

* If <math>a_n \equiv 0\text{ (mod 3)}</math>, then <math>a_{n+1}=\frac{a_n}{3}+2^n+1</math>.
* If <math>a_n \equiv 2\text{ (mod 3)}</math>, then <math>a_{n+1}=\frac{a_n-2}{3}+2^n-1</math>.

With these two rules alone, Bonnie calculates the first few terms in the sequence: <math>2, 0, 3, 6, 11, 18, 39, 78, 155, 306, \dots</math>. At this point, Bonnie plans to continue writing terms until a term becomes <math>1\text{ (mod 3)}</math>. If Bonnie sticks to her plan, will she ever finish?

<div class="toccolours mw-collapsible mw-collapsed">'''Solution'''<div class="mw-collapsible-content">
How to guess the closed-form solution: Firstly, notice that <math>a_n \approx \frac{3}{5} \times 2^n</math>. Secondly, calculate the error term <math>a_n - \frac{3}{5} \times 2^n</math>. The error term appears to have a period of 4. This leads to the following guess:

<math display="block">a_n=\frac{3}{5}\begin{cases}
2^n+\frac{7}{3} &\text{if } n\equiv 0 \pmod{4}\\
2^n-2 &\text{if } n\equiv 1 \pmod{4}\\
2^n+1 &\text{if } n\equiv 2 \pmod{4}\\
2^n+2 &\text{if } n\equiv 3 \pmod{4}\\
\end{cases}</math>

This closed-form solution can be proven correct by induction. Unfortunately, the induction may require a lot of tedious calculations.

For all <math>k</math>, we have <math>a_{4k} \equiv 2\text{ (mod 3)}</math> and <math>a_{4k+1} \equiv a_{4k+2} \equiv a_{4k+3} \equiv 0\text{ (mod 3)}</math>. Therefore, Bonnie will never finish.
</div></div>

Main Page

2024-06-28T20:41:51Z

UncombedCoconut:

The [[Busy Beaver function]] BB (called S originally) was introduced by [https://en.wikipedia.org/wiki/Tibor_Rad%C3%B3 Tibor Radó] in 1962 <ref>Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x</ref> for 2-symbol [[Turing machines]] and later generalised<ref>Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.</ref> to m-symbol Turing machines:

{| class="wikitable"
|-
| BB(n,m) = Maximum number of steps taken by a halting n-state, m-symbol Turing machine starting from a blank (all 0) tape
|}

The busy beaver function is not computable and, few of its values are known:

{| class="wikitable"
|+ Small busy beaver values <ref>https://bbchallenge.org/~pascal.michel/ha.html</ref> <ref name=":0">https://bbchallenge.org/</ref>
|-
| || 2-state || 3-state || 4-state || 5-state || 6-state || 7-state
|-
| 2-symbol
| [[BB(2)]] = 6
| [[BB(3)]] = 21
| [[BB(4)]] = 107
| [[BB(5)]] = 47,176,870
| style="background: orange;" | [[BB(6)]] > <math>10 \uparrow \uparrow 15</math>
| style="background: orange;" | [[BB(7)]]
|-
| 3-symbol || [[BB(2,3)]] = 38
| style="background: orange;" | [[BB(3,3)]] > <math>10^{17}</math>
| style="background: #ffe4b2;" | [[BB(4,3)]] > <math>10^{14072}</math>
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
| 4-symbol
| [[BB(2,4)]] = 3,932,964
| style="background: #ffe4b2;" | [[BB(3,4)]] ≥ <math>2 \uparrow^{15} 5 + 14</math>
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
| 5-symbol
| style="background: orange;" | [[BB(2,5)]] > 6.5 × <math>10^{38033}</math>
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |

|}

In the above table, <span style="background: orange">cells are highlighted in orange</span> when there are known [[Cryptids]] (mathematically-hard machines) in that class.

== bbchallenge.org ==
[[bbchallenge.org]] <ref name=":0" /> is a massively collaborative research project whose general goal is to obtain more knowledge on the [[Busy Beaver function]]. In practice, it mainly consists in collaboratively building [[Deciders]], programs that automatically prove that some Turing machines do not halt. Other efforts also include:

* Formalising results using theorem provers (such as [https://en.wikipedia.org/wiki/Coq_(software) Coq])
* Maintaining [[Holdouts lists]] for small busy beaver values
* Proving the behavior of [[:Category:Individual Machines|Individual machines]]
* Finding [[Cryptids]] (mathematically-hard machines)
* Building [[Accelerated Simulator]]s to simulate halting machines faster

Notably, as part of bbchallenge.org, in June 2024 the 5th busy beaver value [[BB(5)]] was proven in Coq to be equal to the lower bound found in 1989<ref>H. Marxen and J. Buntrock. Attacking the Busy Beaver 5.
Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>: 47,176,870.

== Contribute to this wiki ==
This wiki is collaborative, feel free to contribute by editing existing pages or creating new ones:

<inputbox>
type=create
width=100
break=no
buttonlabel=Create new article
default=(Article title)
</inputbox>

==Notes==
<references />

Cryptids

2024-06-28T20:39:30Z

UncombedCoconut: Add the BB(6) critter, which might be named.

'''Cryptids''' are Turing Machines whose behavior (when started on a blank tape) can be described completely by a relatively simple mathematical rule, but where that rule falls into a class of unsolved (and presumed hard) mathematical problems. This definition is somewhat subjective (What counts as a simple rule? What counts as a hard problem?). In practice, most currently known small Cryptids have [[Collatz-like]] behavior. In other words, the halting problem from blank tape of cryptids is mathematically-hard.

If there exists a Cryptid with n states and m symbols, then BB(n, m) cannot be solved without solving this hard math problem.

The name Cryptid was proposed by Shawn Ligocki in an Oct 2023 [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html blog post] announcing the discovery of [[Bigfoot]].

== List of Cryptids ==

{| class="wikitable"
|-
! Name !! BB domain !! Machine !! Announcement !! Date !! Discoverer !! Note
|-
|RH
|BB(744)
|https://github.com/sorear/metamath-turing-machines/blob/master/riemann-matiyasevich-aaronson.nql
|
|2016
|Matiyasevich and O’Rear
|The machine halts if and only if [https://en.wikipedia.org/wiki/Riemann_hypothesis Riemann Hypothesis] is false.
|-
|Goldbach
|BB(27)
|https://gist.github.com/anonymous/a64213f391339236c2fe31f8749a0df6<nowiki/>(unverified)
|
|2016
|anonymous
|The machine halts if and only if [https://en.wikipedia.org/wiki/Goldbach%27s_conjecture Golbach's conjecture] is false. To the best of our knowledge this construction has not been independently verified.
|-
| Erdős || BB(5,4) and
BB(15)
|
https://docs.bbchallenge.org/other/powers_of_two_5_4.txt

https://docs.bbchallenge.org/other/powers_of_two_15_2.txt
|| [https://arxiv.org/abs/2107.12475 arxiv preprint] || Jul 2021 || [[User:Cosmo|Tristan Stérin]] (<code>@cosmo</code>) and Damien Woods || The machine halts if and only if the following conjecture by Erdős is false: "For all n > 8, there is at least one 2 in the base-3 representation of 2^n"
|-
|Weak Collatz
|BB(124) and BB(43,4)
|https://docs.bbchallenge.org/other/weak_Collatz_conjecture_124_2.txt (unverified)
https://docs.bbchallenge.org/other/weak_Collatz_conjecture_43_4.txt (unverified)
|
|Jul 2021
|[[User:Cosmo|Tristan Stérin]]
|The machine halts if and only if the "weak Collatz conjecture" is false. The weak Collatz conjecture states that the iterated Collatz map (3x+1) has only one cycle on the positive integers.
Not independently verified, and probably easy to further optimise.
|-
| [[Bigfoot]]|| [[BB(3, 3)]]|| <code>1RB2RA1LC_2LC1RB2RB_---2LA1LA</code>|| [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3, 3) is hard] || Nov 2023 || [[User:Sligocki|Shawn Ligocki]] ||
|-
| [[Hydra]]|| [[BB(2, 5)]]|| <code>1RB3RB---3LA1RA_2LA3RA4LB0LB0LA</code>|| [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2, 5) is hard] || May 2024 || Daniel Yuan ||
|-
| || BB(2, 5) || <code>1RB3RB---3LA1RA_2LA3RA4LB0LB1LB</code>||[https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html#a-bonus-cryptid A Bonus Cryptid] || May 2024 || Daniel Yuan ||
|-
| [[Bigfoot]] - compiled|| [[BB(7, 2)|BB(7)]]|| <code>0RB1RB_1LC0RA_1RE1LF_1LF1RE_0RD1RD_1LG0LG_---1LB</code>|| [https://github.com/sligocki/sligocki.github.io/issues/8#issuecomment-2140887228 Bigfoot Comment] || June 2024 || <code>@Iijil1</code>|| Compilation of Bigfoot into 2 symbols, there was a previous compilation [https://github.com/sligocki/sligocki.github.io/issues/8#issuecomment-1774200442 with 8 states]
|-
|
|BB(6)
|[[0RB0LD_1LC0LI_1LD1LB_0LE0RG_1RF0RH_1RA---_0RD0LB_0RA---_0RF1RZ]]
|[https://discord.com/channels/960643023006490684/1026577255754903572/1256223215206924318 Discord message]
|June 2024
|<code>@mxdys</code>
|Iteration similar to Hydra with modified accumulation.
|-
|[[Hydra]] - compiled
|BB(9)
|<pre>
0RB0LD_1LC0LI_1LD1LB_0LE0RG_1RF0RH_1RA---_0RD0LB_0RA---_0RF1RZ
</pre>[[File:Hydra_9_states.txt]]
|[https://discord.com/channels/960643023006490684/1084047886494470185/1251572501578780782 Discord message]
|June 2024
|<code>@Iijil1</code>
|Compilation of Hydra into 2 symbols, all[https://discord.com/channels/960643023006490684/1084047886494470185/1253193750486974464 confirmed by Shawn Ligocki].
<small>[https://discord.com/channels/960643023006490684/1084047886494470185/1247560072427474955 Previous compilation had 10 states], by Daniel Yuan, also [https://discord.com/channels/960643023006490684/1084047886494470185/1247579473042346136 confirmed by Shawn Ligocki].</small> |}

== Beeping Busy Beaver ==

Cryptids were actually noticed in the [[Beeping Busy Beaver]] problem before they were in the classic Busy Beaver. See [https://www.sligocki.com/2022/04/03/mother-of-giants.html Mother of Giants] describing a "family" of Turing machines which "probviously" quasihalt, but requires solving a Collatz-like problem in order to actually prove it. They are all TMs formed by filling in the missing transition in <code>1RB1LE_0LC0LB_0LD1LC_1RD1RA_---0LA</code> with different values.

1RB1RA 0LC1LE 1LD1LC 1LA0LB 1LF1RE ---0RA

2024-06-28T20:10:50Z

UncombedCoconut: oops, iterations run was off by a factor of 10.

{{machine|1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA}}
This machine was the first identified [[BB(6)]] Collatz-like [[Cryptid]], and is closely related to [[Hydra]].

It simulates the Collatz-like iteration

<math display="block">\begin{array}{l}
A(2a, & b) & \to & A(3a, & b+2) \\
A(2a+1, & b) & \to & A(3a+1, & b-1) & \text{if} & b>0 \\
A(2a+1, & 0) & \to & \text{HALT}
\end{array}</math>
<br>
starting from A(8, 0),
<br>
using configurations of the form <nowiki>A(a+4, b) = ^ 1^b 0 1^a E> $</nowiki>

It was discovered by mxdys on 28 Jun 2024 and shared on Discord [https://discord.com/channels/960643023006490684/1026577255754903572/1256223215206924318].

Compared to the [[Hydra]] iteration, this one starts at (8, 0) rather than (3, 0), and the roles of odd and even a are exchanged (in terms of which increases b by two, and which decrements b or halts).
Obstacles to proving the long-run behavior are equally serious.
Like the [[Hydra]] iteration, this one is biased toward increasing the value of b (assuming equal chances of adding +2 or -1). There is no halt in the first one million iterations, by which point b has reached 498503.

1RB1RA 0LC1LE 1LD1LC 1LA0LB 1LF1RE ---0RA

2024-06-28T19:37:57Z

UncombedCoconut: Improved usage of Ye Olde Wiki Markup

{{machine|1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA}}
This machine was the first identified [[BB(6)]] Collatz-like [[Cryptid]], and is closely related to [[Hydra]].

It simulates the Collatz-like iteration

<math display="block">\begin{array}{l}
A(2a, & b) & \to & A(3a, & b+2) \\
A(2a+1, & b) & \to & A(3a+1, & b-1) & \text{if} & b>0 \\
A(2a+1, & 0) & \to & \text{HALT}
\end{array}</math>
<br>
starting from A(8, 0),
<br>
using configurations of the form <nowiki>A(a+4, b) = ^ 1^b 0 1^a E> $</nowiki>

It was discovered by mxdys on 28 Jun 2024 and shared on Discord [https://discord.com/channels/960643023006490684/1026577255754903572/1256223215206924318].

Compared to the [[Hydra]] iteration, this one starts at (8, 0) rather than (3, 0), and the roles of odd and even a are exchanged (in terms of which increases b by two, and which decrements b or halts).
Obstacles to proving the long-run behavior are equally serious.
Like the [[Hydra]] iteration, this one is biased toward increasing the value of b (assuming equal chances of adding +2 or -1). There is no halt in the first ten million iterations, by which point b has reached 498503.

1RB1RA 0LC1LE 1LD1LC 1LA0LB 1LF1RE ---0RA

2024-06-28T19:34:30Z

UncombedCoconut:

{{machine|1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA}}
This machine was the first identified [[BB(6)]] Collatz-like [[Cryptid]], and is closely related to [[Hydra]].

It simulates the Collatz-like iteration

<math display="block">\begin{array}{l}
A(2a, & b) & \to & A(3a, & b+2) \\
A(2a+1, & b) & \to & A(3a+1, & b-1) & \text{if} & b>0 \\
A(2a+1, & 0) & \to & \text{HALT}
\end{array}</math>
<br>
starting from <pre>A(8, 0)</pre>,
<br>
using configurations of the form <pre>A(a+4, b) = ^ 1^b 0 1^a E> $</pre>

It was discovered by mxdys on 28 Jun 2024 and shared on Discord [https://discord.com/channels/960643023006490684/1026577255754903572/1256223215206924318].

Compared to the [[Hydra]] iteration, this one starts at (8, 0) rather than (3, 0), and the roles of odd and even <pre>a</pre> are exchanged (in terms of which increases <pre>b</pre> by two, and which decrements <pre>b</pre> or halts).
Obstacles to proving the long-run behavior are equally serious.
Like the [[Hydra]] iteration, this one is biased toward increasing the value of <pre>b</pre> (assuming equal chances of adding +2 or -1). There is no halt in the first ten million iterations, by which point <pre>b</pre> has reached 498503.

1RB0RF 1RC0LD 1LB1RC ---0LE 1RA1LE ---0RC

2024-06-23T18:21:58Z

UncombedCoconut:

{{machine|1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC}}

https://bbchallenge.org/1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC

A machine on the critical path to proving the busy beaver value "BB(6, 2, 2)" (6-state, 2-symbol, 2 undefined transitions).
(Machines [[1RB0RB_1LC1RB_---0LD_1RA0LE_1RF1LE_---0RA]], [[1RB1LA_1LA0RC_---0RD_1LE1RD_0LA0LF_---0LA]], and [[1RB1LA_1LA0RC_---0RD_1LE1RD_1LB0LF_---0LA]] <ref>The [[Holdout lists|holdout list]] omits the last one. Since holdout lists are useless, it's unspecified whether this case was easier or pruned.</ref> appear to be in the same category.)

The machine behaves as a double counter in base 2; at key steps, the left and right tapes are and must be mirror images (aside from a terminal "1" on the right).
It's easily proven infinite as follows by forward analysis: we can define a CFL [https://en.wikipedia.org/wiki/Context-free_language] where <L> shows the rule "0(11)*1B1 -> (11)*1C>", and <M> is a [[Closed Set|closed language]] for the TM:
<pre>
<L> ::= 0(11)*(1B1|D10)
| 0(11)*(1E1|E11)(11)*00
| E0(11)*00
| 1A00|11B0
| (1A11|10F1)(11)*00
| 100(11)*(C11|1C1)(11)*00
| 100(11)*C00
| 10B010|101C10|1011C0|101B11|10D101|1E0001|11A001|111B01|1111C1
| 10<L>10
| 10(11)*(1C10|11C0)
| 1<L>1
| 1(11)*1C1

<M> ::= A0|1B0
| (11)*11C0
| <L>1
| (11)*1(C1|1C0)
</pre>

In particular, <L> includes 10<L>10 and 1<L>1, but not for example 1<L>10; indeed, a config of the form (1<L>10)1 will halt the TM.
It therefore provides an example of "BB(6, 2, 2)" needing an inductive or closed-language decider stronger than (weighted) finite automata methods.

Note: A simpler multi-symbol example of the phenomenon is https://bbchallenge.org/1RB2LA0LA_1LA2RC0RC_---2RB0RB, with the rule "bin(n) <A reversed(bin(n)) |- bin(n+1) <A reversed(bin(n+1))".

1RB0RF 1RC0LD 1LB1RC ---0LE 1RA1LE ---0RC

2024-06-23T18:11:21Z

UncombedCoconut: Created page with "{{machine|1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC}} https://bbchallenge.org/1RB0RF_1RC0LD_1LB1RC_---0LE_1RA1LE_---0RC A machine on the critical path to proving the busy beaver value "BB(6, 2, 2)" (6-state, 2-symbol, 2 undefined transitions). (Machines 1RB0RB_1LC1RB_---0LD_1RA0LE_1RF1LE_---0RA, 1RB1LA_1LA0RC_---0RD_1LE1RD_0LA0LF_---0LA, and 1RB1LA_1LA0RC_---0RD_1LE1RD_1LB0LF_---0LA <ref>The holdout list omits the last one. Since holdout l..."

Code repositories

2024-05-29T12:12:21Z

UncombedCoconut: Created page with "This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them. * [https://github.com/bbchallenge/bbchallenge-deciders The official bbchallenge deciders repo] * [https://github.com/ccz181078/Coq-BB5 Coq-BB5 by @mxdys] * [https://github.com/meithecatte/busycoq A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei]..."

This is a stub, to be expanded to a family of pages (probably) explaining the deciders' capabilities and other info about them.

* [https://github.com/bbchallenge/bbchallenge-deciders The official bbchallenge deciders repo]
* [https://github.com/ccz181078/Coq-BB5 Coq-BB5 by @mxdys]
* [https://github.com/meithecatte/busycoq A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs, by @mei]
* [https://skelet.ludost.net/bb/ bbfind by Skelet] wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord]
* [https://gist.github.com/mateon1/6cdad07e15f6acf992b79dc2baf0492c Accelerated TM simulators in Python utilizing memoization (like HashLife), by @Mateon1]
* [https://gist.github.com/mateon1/7f5e10169abbb50d1537165c6e71733b Forward segment TM decider by @Mateon1 (variant of Halting Segment)]
* [https://gist.github.com/mateon1/b63eabc371ac35e2a14a9c5ce37413bc Closed Position Set (CPS) TM decider by @Mateon1]
* [https://gist.github.com/mateon1/c801565e499be605cea1283a5984b4c3 SAT Solver CTL code by @Mateon1; TODO dependencies still in Discord posts]
* [https://gist.github.com/savask/1c43a0e5cdd81229f236dcf2b0611c3f The closed position set decider, reverse-engineered from Skelet's program, by @savask]
* [https://gist.github.com/savask/888aa5e058559c972413790c29d7ad72 Bouncers decider, by @savask]
* [https://gist.github.com/savask/c7546bb6384984b2fb3cb90fc7925697 Reproduction of mxdys' repeated blocks decider, by @savask]
* [https://github.com/colette-b/bbchallenge The first SAT-based CTL/FAR decider, by @djmati1111]
* [https://github.com/FransFaase/SymbolicTM An early CTL verifier (regex-based) by Frans Faase]
* [https://github.com/Iijil1/Bouncers Bouncers decider, by @Iijil]
* [https://github.com/Iijil1/Bruteforce-CTL Bruteforce-CTL decider, by @Iijil]
* [https://github.com/Iijil1/MITMWFAR Meet-in-the-Middle Weighted Finite Automata... Reduction... by @Iijil]
* [https://github.com/int-y1/proofs/tree/master/BusyLean Some progress toward a FAR verifier checked by Lean, by @-d]
* [https://github.com/LegionMammal978/bigfoot-sim An accelerated simulator for the "Bigfoot" TM, by @LegionMammal978]
* [https://github.com/Nathan-Fenner/bbchallenge-dafny-deciders Deciders formally verified using Dafny, by @nathanf]
* [https://github.com/Nathan-Fenner/bbchallenge-regexy-decider CTL decider by @nathanf]
* [https://github.com/Nathan-Fenner/bb-simple-n-gram-cps A dramatic simplification of CPS (much less resource-intensive and not as strong) by @nathanf]
* [https://github.com/Nathan-Fenner/busy-beaver-dafny-regex-verifier A formally verified CTL checker by @nathanf]
* https://github.com/nickdrozd/busy-beaver-stuff
* https://github.com/phinanix/busy-beavers
* https://github.com/sligocki/busy-beaver
* https://github.com/TonyGuil/bbchallenge
* https://github.com/uncombedcoconut/bbchallenge
* https://github.com/UncombedCoconut/bbchallenge-deciders/tree/FARther/decider-finite-automata-reduction
* https://github.com/UncombedCoconut/bbchallenge-nfa-verification
* https://github.com/univerz/bbc

* [https://github.com/danbriggs/Turing TM proofs/writing by Dan Briggs]