BusyBeaverWiki - User contributions [en]

TMBR: November 2026

2026-11-09T04:24:44Z

Svennik: /* Cryptids */

{{TMBRnav|October 2026|December 2026}}''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''

[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026.

== Media ==

* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026.

== BB Adjacent ==
* [[Pebble Automaton]]
** On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.

== Champions ==
{| class="wikitable mw-collapsible mw-collapsed"
|+New''' '''champions''' '''discovered''' '''this''' '''month
!Domain
!Champion
!Discoverer
!New''' '''lower''' '''bound
!Discoverer
!Previous''' '''lower''' '''bound
|-
|BB(17)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}}
| rowspan="2" |Jeff Ketchersid
|<math>f_{\omega + 3}^3(9)</math>
|-
|BB(18)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}}
|<math>f_{\omega + 3}^4(9)</math>
|Jeff Ketchersid
|<math>f_{\omega + 3}(114)</math>
|-
|BB(19)
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}}
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 7}^2(5)</math>
|-
|BB(20)
|{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}}
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math>
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 6}^2(4)</math>
|-
|BB(11,4)
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}}
| rowspan="9" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(21)</math>
|<math>f_{\omega + 3}^2(4)</math>
|-
|BB(8,5)
|{{TM|2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH|halt}}
|<math>f_{\omega \cdot 2 + 1}(93)</math>
| rowspan="2" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(32)</math>
|-
|BB(4,6)
|{{TM|5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD|halt}}
|<math>f_{\omega + 2}(29)</math>
|<math>f_{\omega + 1}(2 \uparrow^{15} 5)</math>
|-
|BB(5,6)
|{{TM|1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE|halt}}
|<math>f_{\omega + 3}(31)</math>
|-
|BB(6,6)
|{{TM|4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB|halt}}
|<math>f_{\omega * 2}(89)</math>
|-
|BB(7,6)
|{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}}
|<math>f_{\omega^2}(63)</math>
|-
|BB(8,6)
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}}
|<math>f_{\omega^2 + 1}(7)</math>
|-
|BB(3,7)
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}}
|<math>f_{\omega + 1}(77)</math>
|[[User:Loader3229]]
|<math>f_{\omega}^4(15)</math>
|-
|BB(4,7)
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}}
|<math>f_{\omega + 2}(124)</math>
|}

* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds:
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317] and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>.
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>.
** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math>
* [[User:Jacobzheng]] discovered the following bounds:
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>.
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>.
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>.

== Holdouts ==
{| class="wikitable"
|+'''BB Holdout Reduction by Domain'''
!Domain
!New Holdout Count
!Previous Holdout Count
!Holdout Reduction
!% Reduction
|-
|[[BB(6)]]
|608
|608
|0
|0.00%
|-
|[[BB(2,5)]]
|37 (official)
|59 (official), 37 (informal)
|22 (Rocq confirmation of Lean proofs)
|37.29% (confirmations)
|}

* [[BB(6)]]
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]
*[[BB(2,5)]]
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]

== Cryptids ==
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.

* [[Cryptids#Cryptids at the Edge|Cryptids in the Wild]] (+ [[User:RobinCodes/Machines at the Edge|Energy Vampires]])
** [https://discord.com/channels/960643023006490684/1561037362581086228 Reus Vampires]
*** On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![https://discord.com/channels/960643023006490684/1561037362581086228/1566292773173198980] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.

* [[Cryptids#Larger Cryptids|Larger Cryptids]]
** [[Logical independence|Logical Independence]]
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]]
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
***[[wikipedia:New_foundations|New Foundations]]
****On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied by a Lean proof. This is also the smallest known TM which PA cannot prove is non-halting.
** Computational Complexity Theory
*** On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719]

{| class="wikitable"
|+Other problems encoded into Turing machines this month
!Conjecture
!Domain
!Discoverer
!Discovery date
!Notes
|-
|Pillai's conjecture
|BBBB(91)
|charlie, Claude[https://discord.com/channels/960643023006490684/1385498968011575366/1566248174614479061]
|November 1
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.]
|}
[[Category:This Month in Beaver Research|2026-11]]

TMBR: November 2026

2026-11-09T04:18:36Z

Svennik: /* Cryptids */ PA cannot determine BB(210)

{{TMBRnav|October 2026|December 2026}}''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''

[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026.

== Media ==

* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026.

== BB Adjacent ==
* [[Pebble Automaton]]
** On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.

== Champions ==
{| class="wikitable mw-collapsible mw-collapsed"
|+New''' '''champions''' '''discovered''' '''this''' '''month
!Domain
!Champion
!Discoverer
!New''' '''lower''' '''bound
!Discoverer
!Previous''' '''lower''' '''bound
|-
|BB(17)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}}
| rowspan="2" |Jeff Ketchersid
|<math>f_{\omega + 3}^3(9)</math>
|-
|BB(18)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}}
|<math>f_{\omega + 3}^4(9)</math>
|Jeff Ketchersid
|<math>f_{\omega + 3}(114)</math>
|-
|BB(19)
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}}
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 7}^2(5)</math>
|-
|BB(20)
|{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}}
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math>
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 6}^2(4)</math>
|-
|BB(11,4)
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}}
| rowspan="9" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(21)</math>
|<math>f_{\omega + 3}^2(4)</math>
|-
|BB(8,5)
|{{TM|2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH|halt}}
|<math>f_{\omega \cdot 2 + 1}(93)</math>
| rowspan="2" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(32)</math>
|-
|BB(4,6)
|{{TM|5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD|halt}}
|<math>f_{\omega + 2}(29)</math>
|<math>f_{\omega + 1}(2 \uparrow^{15} 5)</math>
|-
|BB(5,6)
|{{TM|1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE|halt}}
|<math>f_{\omega + 3}(31)</math>
|-
|BB(6,6)
|{{TM|4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB|halt}}
|<math>f_{\omega * 2}(89)</math>
|-
|BB(7,6)
|{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}}
|<math>f_{\omega^2}(63)</math>
|-
|BB(8,6)
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}}
|<math>f_{\omega^2 + 1}(7)</math>
|-
|BB(3,7)
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}}
|<math>f_{\omega + 1}(77)</math>
|[[User:Loader3229]]
|<math>f_{\omega}^4(15)</math>
|-
|BB(4,7)
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}}
|<math>f_{\omega + 2}(124)</math>
|}

* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds:
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317] and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>.
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>.
** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math>
* [[User:Jacobzheng]] discovered the following bounds:
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>.
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>.
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>.

== Holdouts ==
{| class="wikitable"
|+'''BB Holdout Reduction by Domain'''
!Domain
!New Holdout Count
!Previous Holdout Count
!Holdout Reduction
!% Reduction
|-
|[[BB(6)]]
|608
|608
|0
|0.00%
|-
|[[BB(2,5)]]
|37 (official)
|59 (official), 37 (informal)
|22 (Rocq confirmation of Lean proofs)
|37.29% (confirmations)
|}

* [[BB(6)]]
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]
*[[BB(2,5)]]
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]

== Cryptids ==
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.

* [[Cryptids#Cryptids at the Edge|Cryptids in the Wild]] (+ [[User:RobinCodes/Machines at the Edge|Energy Vampires]])
** [https://discord.com/channels/960643023006490684/1561037362581086228 Reus Vampires]
*** On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![https://discord.com/channels/960643023006490684/1561037362581086228/1566292773173198980] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.

* [[Cryptids#Larger Cryptids|Larger Cryptids]]
** [[Logical independence|Logical Independence]]
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]]
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
***[[wikipedia:New_foundations|New Foundations]]
****On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied with a Lean proof. This is also the smallest known TM which PA cannot prove is non-halting.
** Computational Complexity Theory
*** On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719]

{| class="wikitable"
|+Other problems encoded into Turing machines this month
!Conjecture
!Domain
!Discoverer
!Discovery date
!Notes
|-
|Pillai's conjecture
|BBBB(91)
|charlie, Claude[https://discord.com/channels/960643023006490684/1385498968011575366/1566248174614479061]
|November 1
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.]
|}
[[Category:This Month in Beaver Research|2026-11]]

TMBR: November 2026

2026-11-09T04:17:44Z

Svennik: /* Cryptids */

{{TMBRnav|October 2026|December 2026}}''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''

[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026.

== Media ==

* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026.

== BB Adjacent ==
* [[Pebble Automaton]]
** On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.

== Champions ==
{| class="wikitable mw-collapsible mw-collapsed"
|+New''' '''champions''' '''discovered''' '''this''' '''month
!Domain
!Champion
!Discoverer
!New''' '''lower''' '''bound
!Discoverer
!Previous''' '''lower''' '''bound
|-
|BB(17)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}}
| rowspan="2" |Jeff Ketchersid
|<math>f_{\omega + 3}^3(9)</math>
|-
|BB(18)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}}
|<math>f_{\omega + 3}^4(9)</math>
|Jeff Ketchersid
|<math>f_{\omega + 3}(114)</math>
|-
|BB(19)
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}}
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 7}^2(5)</math>
|-
|BB(20)
|{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}}
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math>
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 6}^2(4)</math>
|-
|BB(11,4)
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}}
| rowspan="9" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(21)</math>
|<math>f_{\omega + 3}^2(4)</math>
|-
|BB(8,5)
|{{TM|2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH|halt}}
|<math>f_{\omega \cdot 2 + 1}(93)</math>
| rowspan="2" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(32)</math>
|-
|BB(4,6)
|{{TM|5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD|halt}}
|<math>f_{\omega + 2}(29)</math>
|<math>f_{\omega + 1}(2 \uparrow^{15} 5)</math>
|-
|BB(5,6)
|{{TM|1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE|halt}}
|<math>f_{\omega + 3}(31)</math>
|-
|BB(6,6)
|{{TM|4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB|halt}}
|<math>f_{\omega * 2}(89)</math>
|-
|BB(7,6)
|{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}}
|<math>f_{\omega^2}(63)</math>
|-
|BB(8,6)
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}}
|<math>f_{\omega^2 + 1}(7)</math>
|-
|BB(3,7)
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}}
|<math>f_{\omega + 1}(77)</math>
|[[User:Loader3229]]
|<math>f_{\omega}^4(15)</math>
|-
|BB(4,7)
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}}
|<math>f_{\omega + 2}(124)</math>
|}

* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds:
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317] and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>.
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>.
** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math>
* [[User:Jacobzheng]] discovered the following bounds:
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>.
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>.
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>.

== Holdouts ==
{| class="wikitable"
|+'''BB Holdout Reduction by Domain'''
!Domain
!New Holdout Count
!Previous Holdout Count
!Holdout Reduction
!% Reduction
|-
|[[BB(6)]]
|608
|608
|0
|0.00%
|-
|[[BB(2,5)]]
|37 (official)
|59 (official), 37 (informal)
|22 (Rocq confirmation of Lean proofs)
|37.29% (confirmations)
|}

* [[BB(6)]]
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]
*[[BB(2,5)]]
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]

== Cryptids ==
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.

* [[Cryptids#Cryptids at the Edge|Cryptids in the Wild]] (+ [[User:RobinCodes/Machines at the Edge|Energy Vampires]])
** [https://discord.com/channels/960643023006490684/1561037362581086228 Reus Vampires]
*** On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![https://discord.com/channels/960643023006490684/1561037362581086228/1566292773173198980] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.

* [[Cryptids#Larger Cryptids|Larger Cryptids]]
** [[Logical independence|Logical Independence]]
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]]
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
***[[wikipedia:New_foundations|New Foundations]]
****On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied with a Lean proof. This is also the smallest known TM which PA cannot prove doesn't halt.
** Computational Complexity Theory
*** On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719]

{| class="wikitable"
|+Other problems encoded into Turing machines this month
!Conjecture
!Domain
!Discoverer
!Discovery date
!Notes
|-
|Pillai's conjecture
|BBBB(91)
|charlie, Claude[https://discord.com/channels/960643023006490684/1385498968011575366/1566248174614479061]
|November 1
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.]
|}
[[Category:This Month in Beaver Research|2026-11]]

TMBR: November 2026

2026-11-09T04:14:10Z

Svennik: /* Cryptids */

{{TMBRnav|October 2026|December 2026}}''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''

[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026.

== Media ==

* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026.

== BB Adjacent ==
* [[Pebble Automaton]]
** On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.

== Champions ==
{| class="wikitable mw-collapsible mw-collapsed"
|+New''' '''champions''' '''discovered''' '''this''' '''month
!Domain
!Champion
!Discoverer
!New''' '''lower''' '''bound
!Discoverer
!Previous''' '''lower''' '''bound
|-
|BB(17)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}}
| rowspan="2" |Jeff Ketchersid
|<math>f_{\omega + 3}^3(9)</math>
|-
|BB(18)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}}
|<math>f_{\omega + 3}^4(9)</math>
|Jeff Ketchersid
|<math>f_{\omega + 3}(114)</math>
|-
|BB(19)
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}}
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 7}^2(5)</math>
|-
|BB(20)
|{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}}
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math>
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 6}^2(4)</math>
|-
|BB(11,4)
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}}
| rowspan="9" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(21)</math>
|<math>f_{\omega + 3}^2(4)</math>
|-
|BB(8,5)
|{{TM|2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH|halt}}
|<math>f_{\omega \cdot 2 + 1}(93)</math>
| rowspan="2" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(32)</math>
|-
|BB(4,6)
|{{TM|5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD|halt}}
|<math>f_{\omega + 2}(29)</math>
|<math>f_{\omega + 1}(2 \uparrow^{15} 5)</math>
|-
|BB(5,6)
|{{TM|1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE|halt}}
|<math>f_{\omega + 3}(31)</math>
|-
|BB(6,6)
|{{TM|4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB|halt}}
|<math>f_{\omega * 2}(89)</math>
|-
|BB(7,6)
|{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}}
|<math>f_{\omega^2}(63)</math>
|-
|BB(8,6)
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}}
|<math>f_{\omega^2 + 1}(7)</math>
|-
|BB(3,7)
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}}
|<math>f_{\omega + 1}(77)</math>
|[[User:Loader3229]]
|<math>f_{\omega}^4(15)</math>
|-
|BB(4,7)
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}}
|<math>f_{\omega + 2}(124)</math>
|}

* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds:
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317] and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>.
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>.
** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math>
* [[User:Jacobzheng]] discovered the following bounds:
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>.
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>.
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>.

== Holdouts ==
{| class="wikitable"
|+'''BB Holdout Reduction by Domain'''
!Domain
!New Holdout Count
!Previous Holdout Count
!Holdout Reduction
!% Reduction
|-
|[[BB(6)]]
|608
|608
|0
|0.00%
|-
|[[BB(2,5)]]
|37 (official)
|59 (official), 37 (informal)
|22 (Rocq confirmation of Lean proofs)
|37.29% (confirmations)
|}

* [[BB(6)]]
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]
*[[BB(2,5)]]
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]

== Cryptids ==
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.

* [[Cryptids#Cryptids at the Edge|Cryptids in the Wild]] (+ [[User:RobinCodes/Machines at the Edge|Energy Vampires]])
** [https://discord.com/channels/960643023006490684/1561037362581086228 Reus Vampires]
*** On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![https://discord.com/channels/960643023006490684/1561037362581086228/1566292773173198980] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.

* [[Cryptids#Larger Cryptids|Larger Cryptids]]
** [[Logical independence|Logical Independence]]
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]]
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
***[[wikipedia:New_foundations|New Foundations]]
****On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied with a Lean proof.
** Computational Complexity Theory
*** On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719]

{| class="wikitable"
|+Other problems encoded into Turing machines this month
!Conjecture
!Domain
!Discoverer
!Discovery date
!Notes
|-
|Pillai's conjecture
|BBBB(91)
|charlie, Claude[https://discord.com/channels/960643023006490684/1385498968011575366/1566248174614479061]
|November 1
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.]
|}
[[Category:This Month in Beaver Research|2026-11]]

TMBR: November 2026

2026-11-09T04:12:40Z

Svennik: /* Cryptids */ New Foundations set theory

{{TMBRnav|October 2026|December 2026}}''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''

[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026.

== Media ==

* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026.

== BB Adjacent ==
* [[Pebble Automaton]]
** On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.

== Champions ==
{| class="wikitable mw-collapsible mw-collapsed"
|+New''' '''champions''' '''discovered''' '''this''' '''month
!Domain
!Champion
!Discoverer
!New''' '''lower''' '''bound
!Discoverer
!Previous''' '''lower''' '''bound
|-
|BB(17)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}}
| rowspan="2" |Jeff Ketchersid
|<math>f_{\omega + 3}^3(9)</math>
|-
|BB(18)
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}}
|<math>f_{\omega + 3}^4(9)</math>
|Jeff Ketchersid
|<math>f_{\omega + 3}(114)</math>
|-
|BB(19)
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}}
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 7}^2(5)</math>
|-
|BB(20)
|{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}}
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math>
| rowspan="2" |[[User:Jacobzheng]]
|<math>f_{\omega + 6}^2(4)</math>
|-
|BB(11,4)
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}}
| rowspan="9" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(21)</math>
|<math>f_{\omega + 3}^2(4)</math>
|-
|BB(8,5)
|{{TM|2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH|halt}}
|<math>f_{\omega \cdot 2 + 1}(93)</math>
| rowspan="2" |[[User:Loader3229]]
|<math>f_{\omega \cdot 2}(32)</math>
|-
|BB(4,6)
|{{TM|5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD|halt}}
|<math>f_{\omega + 2}(29)</math>
|<math>f_{\omega + 1}(2 \uparrow^{15} 5)</math>
|-
|BB(5,6)
|{{TM|1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE|halt}}
|<math>f_{\omega + 3}(31)</math>
|-
|BB(6,6)
|{{TM|4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB|halt}}
|<math>f_{\omega * 2}(89)</math>
|-
|BB(7,6)
|{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}}
|<math>f_{\omega^2}(63)</math>
|-
|BB(8,6)
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}}
|<math>f_{\omega^2 + 1}(7)</math>
|-
|BB(3,7)
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}}
|<math>f_{\omega + 1}(77)</math>
|[[User:Loader3229]]
|<math>f_{\omega}^4(15)</math>
|-
|BB(4,7)
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}}
|<math>f_{\omega + 2}(124)</math>
|}

* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds:
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317] and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>.
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>.
** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math>
* [[User:Jacobzheng]] discovered the following bounds:
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>.
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>.
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>.

== Holdouts ==
{| class="wikitable"
|+'''BB Holdout Reduction by Domain'''
!Domain
!New Holdout Count
!Previous Holdout Count
!Holdout Reduction
!% Reduction
|-
|[[BB(6)]]
|608
|608
|0
|0.00%
|-
|[[BB(2,5)]]
|37 (official)
|59 (official), 37 (informal)
|22 (Rocq confirmation of Lean proofs)
|37.29% (confirmations)
|}

* [[BB(6)]]
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]
*[[BB(2,5)]]
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]

== Cryptids ==
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.

* [[Cryptids#Cryptids at the Edge|Cryptids in the Wild]] (+ [[User:RobinCodes/Machines at the Edge|Energy Vampires]])
** [https://discord.com/channels/960643023006490684/1561037362581086228 Reus Vampires]
*** On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![https://discord.com/channels/960643023006490684/1561037362581086228/1566292773173198980] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.

* [[Cryptids#Larger Cryptids|Larger Cryptids]]
** [[Logical independence|Logical Independence]]
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]]
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
**** On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied with a Lean proof.
** Computational Complexity Theory
*** On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719]

{| class="wikitable"
|+Other problems encoded into Turing machines this month
!Conjecture
!Domain
!Discoverer
!Discovery date
!Notes
|-
|Pillai's conjecture
|BBBB(91)
|charlie, Claude[https://discord.com/channels/960643023006490684/1385498968011575366/1566248174614479061]
|November 1
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.]
|}
[[Category:This Month in Beaver Research|2026-11]]

Logical independence

2026-11-09T02:50:38Z

Svennik: /* History */ connect to PA

[[File:Independencechart.png|thumb|A chart showing which busy beaver numbers are independent of theories. Modification of a chart from a Vsauce video.]]
For any recursively enumerable and arithmetically sound axiomatic theory T, there exists an integer <math>N_T</math> such that T cannot prove the values of BB(n) for any <math>n \ge N_T</math>. For [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo–Fraenkel set theory]] (ZF), this value is known to be in the range:

<math display="block">6 \le N_{ZF} \le 215</math>

This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> The upper bound comes from an explicit TM which enumerates all possible proofs in ZF and halts if it finds a proof 0 = 1. Assuming ZF is consistent and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts.

Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey that <math>N_{ZF} \le 20</math> and <math>N_{PA} \le 10</math>, where <math>PA</math> refers to the theory of [https://en.wikipedia.org/wiki/Peano%20axioms Peano Arithmetic]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<ref name=":0">Scott Aaronson. 2020. [https://www.scottaaronson.com/papers/bb.pdf The Busy Beaver Frontier]. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369</ref>

== Axiom of Choice ==
Due to [[wikipedia:Absoluteness_(logic)#Shoenfield's_absoluteness_theorem|Shoenfield's absoluteness theorem]], it is known that any TM proven non-halting in ZFC can also be proven non-halting in ZF (and the converse is trivially true), therefore

<math display="block">N_{ZFC} = N_{ZF}</math>

Therefore we refer to ZF and <math>N_{ZF}</math> throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.

== History ==
In a broad sense, the concept of a mechanical or computable procedure that was equivalent to the consistency of a formal theory was discovered by Kurt Gödel's incompleteness theorem, which is notable for a form of meta-mathematical encoding of the statement that "T can prove statement S" (the provability predicate) which is used in all these machines. This was further clarified by Alan Turing and Alonzo Church's work on a formal definition of computability.

Although not a traditional turing machine, in 2012 Merlin Carl and Boris Z. Moroz constructed a [[Diophantine Equation]] which had solutions if and only if NBG (Von Neumann–Bernays–Gödel set theory) is inconsistent. NBG is a conservative extension of ZFC, so solving this equation is independent of ZFC.<ref>Carl, M., & Moroz, B. Z. (2012). ''On a Diophantine representation of the predicate of provability.'' Zapiski Nauchnykh Seminarov POMI, 407, 77-104. (Republished in 2014 in the Journal of Mathematical Sciences) [https://webdoc.sub.gwdg.de/ebook/serien/e/mpi_mathematik/2006/129.pdf (preprint)]</ref>

There is no one authoritative source on the history of TMs independent of ZF, this is our best understanding of the history of TMs found. Mostly these are taken from Scott Aaronson's blog announcements and Busy Beaver Frontier or self-reported by the individuals who discovered them. The Aaronson-Yedida machine used a compiler called ''Laconic'', which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.

Note that only the results with a linked formal verification are known to have such a verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.
{| class="wikitable"
|+History of ZF independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|7910
|May 2016
|Adam Yedidia and Scott Aaronson
|Yedidia and Aaronson 2016<ref>A. Yedidia and S. Aaronson. A relatively small Turing machine whose behavior is independent of set theory. Complex Systems, (25):4, 2016. https://arxiv.org/abs/1605.04343</ref>
|
|-
|1919
|15 May 2016
|Stefan O'Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2016-zf-sorear-1919/zf.nql Github NQL file], [https://groups.google.com/g/metamath/c/OumBq83Ksqs/m/FogyOlLIBwAJ Metamath Group Announcement]
|
|-
|748
|May 2016
|Stefan O’Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL], Busy Beaver Frontier<ref name=":0" />
|
|-
|745
|July 2023
|Johannes Riebel
|Riebel 2023 Bachelor Thesis<ref>Riebel, Johannes (March 2023). ''[https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf The Undecidability of BB(748): Understanding Gödel's Incompleteness Theorems]'' (PDF) (Bachelor's thesis). University of Augsburg.</ref>
|
|-
|643
|July 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL], [https://scottaaronson.blog/?p=8131 Aaronson Announcement]
|
|-
|636
|31 August 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL] ([https://github.com/CatsAreFluffy/metamath-turing-machines/commit/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1 commit])
|
|-
|588
|12 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/30d2e3194866615f68dd2f5101cb300fb039adca commit])
|
|-
|549
|16 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/5d676aec074a94f598959cb3b7733a8f7781762f commit])
|
|-
|432
|19 Aug 2025
|Andrew J. Wade
|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]
|
|-
|335
|11 Oct 2026
|Jeff Ketchersid
|[https://discord.com/channels/960643023006490684/1331570843829932063/1559077555158392844 discord message]
|
|-
|254
|13 Oct 2026
|[https://x.com/_mira___mira_ Mira] with use of ChatGPT, formalized by [https://github.com/jeff87654 Jeff Ketchersid] with Claude
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
|-
|230
|19 Oct 2026
|[https://x.com/ElliotGlazer Elliot Glazer] with use of ChatGPT, formalized with GPT and Claude
|[https://github.com/elliotglazer/k230-rocq Github]
|[https://github.com/elliotglazer/k230-rocq Rocq file]
|-
|215
|21 Oct 2026
|[[wikipedia:Cleo_(mathematician)|Vladimir Reshetnikov]] formalized with Claude
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal Github]
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 Rocq file]
|}
[[File:ZFC Machine 254.png|thumb|The transition table of the machine with 254 states. The initial state is 1.]]
Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.

=== New Foundations (NF) ===
A November 2026 research development gives a 210-working-state, two-symbol Turing machine designed to halt exactly when a fixed first-order presentation of Quine's New Foundations (NF) has a contradiction proof. The archive contains an external Lean 4.35.0 formalization and a source-only verification package.

The source files and past verification receipts are published at [https://github.com/wlad-svennik/notes/tree/main/nf-bb210 GitHub]. The original machine has 210 working states, 420 binary transition rows, and SHA-256 <code>129fc1fe44f609c18c2dfbc6df367835bbee7d6a02bbda3480b93d3c2c52646a</code>. The statement is formalized as an ''external'' Lean metatheorem rather than a completed PA-internal derivation. As of this publication, a fresh independent clean build and community review have not been reported.

=== Peano Arithmetic (PA) ===
For Peano Arithmetic, the ZF and NF independent machines are upper bounds. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower [[wikipedia:Equiconsistency#Consistency_strength|consistency strength]]. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(NF)->Con(PA).

{| class="wikitable"
|+History of Peano Arithmetic (PA) independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|372
|11 February 2026
|@LegionMammal978 (Matthew House)
|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github]
|
|}
This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.<ref>https://mathoverflow.net/questions/508137/interpreting-pa-with-only-adjunction-separation/508161</ref>

=== Large cardinals ===
These tables are for theories stronger than ZFC.

{| class="wikitable"
|+History of ZFC + "There exist arbitrarily large subtle cardinals" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|493
|25 February 2026
|@LegionMammal978
|[https://github.com/Saoi2/turing_machine_explorer/blob/main/subtle.tm Github]
|
|}
This machine takes Wade's ZF champion and adds the [[wikipedia:Axiom_of_choice|axiom of Choice]] and a statement from Harvey Friedman (Proposition 4.3 of [https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf "Primitive Independence Results"])<ref>H. Friedman, "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf Primitive Independence Results]" (2002). Accessed February 2026.</ref> which Friedman showed to be equivalent to "There exist arbitrarily large subtle cardinals" over ZFC.

For reference, this theory is between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the [[wikipedia:Large_cardinal|large cardinal hierarchy]] on Wikipedia.

Note: The initial machine produced in 2016 by Yedidia and Aaronson is designed to halt iff a certain statement created by Harvey Friedman is true.<ref name=":0" /> According to Friedman (without a published proof), this statement is independent of the theory "Stationary Ramsey Property" or ''SRP'', which is equiconsistent with the theory <math>ZFC + \{\text{``There is a }k\text{-subtle cardinal``}\mid k\in\N\}</math> which is also between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the large cardinal hierarchy.<ref>tlonuqbar, "[https://mathoverflow.net/questions/508364/what-is-the-consistency-strength-of-srp-stationary-ramsey-property What is the consistency strength of SRP (Stationary Ramsey Property)?]" (2026). MathOverflow post, accessed February 2026.</ref> However, the theory used by the BB(493) machine is also independent of this theory.

{| class="wikitable"
|+History of ZF + "There exists a Berkeley cardinal" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|1399
|8 November 2026
|@Meganeuridae
|[https://github.com/Meganeuridae/large-cardinal-tms/blob/main/berkeley-rocq/machine/machine.tm Github]
|[https://github.com/Meganeuridae/large-cardinal-tms/tree/main/berkeley-rocq/coq/Berkeley Rocq file]
|}

Berkeley cardinals are perhaps the strongest family of large cardinals considered, initially proposed by Hugh Woodin at a lecture at UC Berkeley as an axiom that was "obviously inconsistent".{{Citation needed}} However, no inconsistency has been found and many people now believe it may be consistent. Berkeley cardinals are known to be inconsistent with the axiom of choice.

== Footnotes ==
<references group="footnote"/>

== References ==
<references />

[[Category:Zoology]]

Logical independence

2026-11-09T02:48:01Z

Svennik: /* New Foundations (NF) */ remove unnecessary caveats: NF is provable consistent from ZFC

[[File:Independencechart.png|thumb|A chart showing which busy beaver numbers are independent of theories. Modification of a chart from a Vsauce video.]]
For any recursively enumerable and arithmetically sound axiomatic theory T, there exists an integer <math>N_T</math> such that T cannot prove the values of BB(n) for any <math>n \ge N_T</math>. For [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo–Fraenkel set theory]] (ZF), this value is known to be in the range:

<math display="block">6 \le N_{ZF} \le 215</math>

This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> The upper bound comes from an explicit TM which enumerates all possible proofs in ZF and halts if it finds a proof 0 = 1. Assuming ZF is consistent and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts.

Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey that <math>N_{ZF} \le 20</math> and <math>N_{PA} \le 10</math>, where <math>PA</math> refers to the theory of [https://en.wikipedia.org/wiki/Peano%20axioms Peano Arithmetic]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<ref name=":0">Scott Aaronson. 2020. [https://www.scottaaronson.com/papers/bb.pdf The Busy Beaver Frontier]. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369</ref>

== Axiom of Choice ==
Due to [[wikipedia:Absoluteness_(logic)#Shoenfield's_absoluteness_theorem|Shoenfield's absoluteness theorem]], it is known that any TM proven non-halting in ZFC can also be proven non-halting in ZF (and the converse is trivially true), therefore

<math display="block">N_{ZFC} = N_{ZF}</math>

Therefore we refer to ZF and <math>N_{ZF}</math> throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.

== History ==
In a broad sense, the concept of a mechanical or computable procedure that was equivalent to the consistency of a formal theory was discovered by Kurt Gödel's incompleteness theorem, which is notable for a form of meta-mathematical encoding of the statement that "T can prove statement S" (the provability predicate) which is used in all these machines. This was further clarified by Alan Turing and Alonzo Church's work on a formal definition of computability.

Although not a traditional turing machine, in 2012 Merlin Carl and Boris Z. Moroz constructed a [[Diophantine Equation]] which had solutions if and only if NBG (Von Neumann–Bernays–Gödel set theory) is inconsistent. NBG is a conservative extension of ZFC, so solving this equation is independent of ZFC.<ref>Carl, M., & Moroz, B. Z. (2012). ''On a Diophantine representation of the predicate of provability.'' Zapiski Nauchnykh Seminarov POMI, 407, 77-104. (Republished in 2014 in the Journal of Mathematical Sciences) [https://webdoc.sub.gwdg.de/ebook/serien/e/mpi_mathematik/2006/129.pdf (preprint)]</ref>

There is no one authoritative source on the history of TMs independent of ZF, this is our best understanding of the history of TMs found. Mostly these are taken from Scott Aaronson's blog announcements and Busy Beaver Frontier or self-reported by the individuals who discovered them. The Aaronson-Yedida machine used a compiler called ''Laconic'', which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.

Note that only the results with a linked formal verification are known to have such a verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.
{| class="wikitable"
|+History of ZF independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|7910
|May 2016
|Adam Yedidia and Scott Aaronson
|Yedidia and Aaronson 2016<ref>A. Yedidia and S. Aaronson. A relatively small Turing machine whose behavior is independent of set theory. Complex Systems, (25):4, 2016. https://arxiv.org/abs/1605.04343</ref>
|
|-
|1919
|15 May 2016
|Stefan O'Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2016-zf-sorear-1919/zf.nql Github NQL file], [https://groups.google.com/g/metamath/c/OumBq83Ksqs/m/FogyOlLIBwAJ Metamath Group Announcement]
|
|-
|748
|May 2016
|Stefan O’Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL], Busy Beaver Frontier<ref name=":0" />
|
|-
|745
|July 2023
|Johannes Riebel
|Riebel 2023 Bachelor Thesis<ref>Riebel, Johannes (March 2023). ''[https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf The Undecidability of BB(748): Understanding Gödel's Incompleteness Theorems]'' (PDF) (Bachelor's thesis). University of Augsburg.</ref>
|
|-
|643
|July 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL], [https://scottaaronson.blog/?p=8131 Aaronson Announcement]
|
|-
|636
|31 August 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL] ([https://github.com/CatsAreFluffy/metamath-turing-machines/commit/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1 commit])
|
|-
|588
|12 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/30d2e3194866615f68dd2f5101cb300fb039adca commit])
|
|-
|549
|16 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/5d676aec074a94f598959cb3b7733a8f7781762f commit])
|
|-
|432
|19 Aug 2025
|Andrew J. Wade
|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]
|
|-
|335
|11 Oct 2026
|Jeff Ketchersid
|[https://discord.com/channels/960643023006490684/1331570843829932063/1559077555158392844 discord message]
|
|-
|254
|13 Oct 2026
|[https://x.com/_mira___mira_ Mira] with use of ChatGPT, formalized by [https://github.com/jeff87654 Jeff Ketchersid] with Claude
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
|-
|230
|19 Oct 2026
|[https://x.com/ElliotGlazer Elliot Glazer] with use of ChatGPT, formalized with GPT and Claude
|[https://github.com/elliotglazer/k230-rocq Github]
|[https://github.com/elliotglazer/k230-rocq Rocq file]
|-
|215
|21 Oct 2026
|[[wikipedia:Cleo_(mathematician)|Vladimir Reshetnikov]] formalized with Claude
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal Github]
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 Rocq file]
|}
[[File:ZFC Machine 254.png|thumb|The transition table of the machine with 254 states. The initial state is 1.]]
Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.

For Peano Arithmetic, the ZF independent machines are an upper bound. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower [[wikipedia:Equiconsistency#Consistency_strength|consistency strength]]. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(PA).

{| class="wikitable"
|+History of Peano Arithmetic (PA) independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|372
|11 February 2026
|@LegionMammal978 (Matthew House)
|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github]
|
|}
This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.<ref>https://mathoverflow.net/questions/508137/interpreting-pa-with-only-adjunction-separation/508161</ref>

=== New Foundations (NF) ===
A November 2026 research development gives a 210-working-state, two-symbol Turing machine designed to halt exactly when a fixed first-order presentation of Quine's New Foundations (NF) has a contradiction proof. The archive contains an external Lean 4.35.0 formalization and a source-only verification package.

The source files and past verification receipts are published at [https://github.com/wlad-svennik/notes/tree/main/nf-bb210 GitHub]. The original machine has 210 working states, 420 binary transition rows, and SHA-256 <code>129fc1fe44f609c18c2dfbc6df367835bbee7d6a02bbda3480b93d3c2c52646a</code>. The statement is formalized as an ''external'' Lean metatheorem rather than a completed PA-internal derivation. As of this publication, a fresh independent clean build and community review have not been reported.

=== Large cardinals ===
These tables are for theories stronger than ZFC.

{| class="wikitable"
|+History of ZFC + "There exist arbitrarily large subtle cardinals" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|493
|25 February 2026
|@LegionMammal978
|[https://github.com/Saoi2/turing_machine_explorer/blob/main/subtle.tm Github]
|
|}
This machine takes Wade's ZF champion and adds the [[wikipedia:Axiom_of_choice|axiom of Choice]] and a statement from Harvey Friedman (Proposition 4.3 of [https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf "Primitive Independence Results"])<ref>H. Friedman, "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf Primitive Independence Results]" (2002). Accessed February 2026.</ref> which Friedman showed to be equivalent to "There exist arbitrarily large subtle cardinals" over ZFC.

For reference, this theory is between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the [[wikipedia:Large_cardinal|large cardinal hierarchy]] on Wikipedia.

Note: The initial machine produced in 2016 by Yedidia and Aaronson is designed to halt iff a certain statement created by Harvey Friedman is true.<ref name=":0" /> According to Friedman (without a published proof), this statement is independent of the theory "Stationary Ramsey Property" or ''SRP'', which is equiconsistent with the theory <math>ZFC + \{\text{``There is a }k\text{-subtle cardinal``}\mid k\in\N\}</math> which is also between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the large cardinal hierarchy.<ref>tlonuqbar, "[https://mathoverflow.net/questions/508364/what-is-the-consistency-strength-of-srp-stationary-ramsey-property What is the consistency strength of SRP (Stationary Ramsey Property)?]" (2026). MathOverflow post, accessed February 2026.</ref> However, the theory used by the BB(493) machine is also independent of this theory.

{| class="wikitable"
|+History of ZF + "There exists a Berkeley cardinal" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|1399
|8 November 2026
|@Meganeuridae
|[https://github.com/Meganeuridae/large-cardinal-tms/blob/main/berkeley-rocq/machine/machine.tm Github]
|[https://github.com/Meganeuridae/large-cardinal-tms/tree/main/berkeley-rocq/coq/Berkeley Rocq file]
|}

Berkeley cardinals are perhaps the strongest family of large cardinals considered, initially proposed by Hugh Woodin at a lecture at UC Berkeley as an axiom that was "obviously inconsistent".{{Citation needed}} However, no inconsistency has been found and many people now believe it may be consistent. Berkeley cardinals are known to be inconsistent with the axiom of choice.

== Footnotes ==
<references group="footnote"/>

== References ==
<references />

[[Category:Zoology]]

Logical independence

2026-11-09T02:46:00Z

Svennik: /* History */

[[File:Independencechart.png|thumb|A chart showing which busy beaver numbers are independent of theories. Modification of a chart from a Vsauce video.]]
For any recursively enumerable and arithmetically sound axiomatic theory T, there exists an integer <math>N_T</math> such that T cannot prove the values of BB(n) for any <math>n \ge N_T</math>. For [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo–Fraenkel set theory]] (ZF), this value is known to be in the range:

<math display="block">6 \le N_{ZF} \le 215</math>

This lower bound comes from the fact that [[BB(5)]] has been proven in Rocq.<ref group="footnote">The fact that this theorem has been proven in Rocq technically does not imply that the theorem must be provable in ZF, because the consistency strength of Rocq is actually higher than that of ZF. However, the BB(5) proof does not use any techniques that could not be formalized within ZF.</ref> The upper bound comes from an explicit TM which enumerates all possible proofs in ZF and halts if it finds a proof 0 = 1. Assuming ZF is consistent and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts.

Harvey Friedman spoke of embedding consistency statements within turing machines in a [https://fomarchive.ugent.be/2004-March/008003.html 2004 posting] on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his [[Busy Beaver Frontier]] survey that <math>N_{ZF} \le 20</math> and <math>N_{PA} \le 10</math>, where <math>PA</math> refers to the theory of [https://en.wikipedia.org/wiki/Peano%20axioms Peano Arithmetic]. Scott also mentioned (crediting Oscar Cunningham for the observation) that if there is an n-state machine that halts if and only if T is inconsistent, then <math>PA</math> + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).<ref name=":0">Scott Aaronson. 2020. [https://www.scottaaronson.com/papers/bb.pdf The Busy Beaver Frontier]. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369</ref>

== Axiom of Choice ==
Due to [[wikipedia:Absoluteness_(logic)#Shoenfield's_absoluteness_theorem|Shoenfield's absoluteness theorem]], it is known that any TM proven non-halting in ZFC can also be proven non-halting in ZF (and the converse is trivially true), therefore

<math display="block">N_{ZFC} = N_{ZF}</math>

Therefore we refer to ZF and <math>N_{ZF}</math> throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.

== History ==
In a broad sense, the concept of a mechanical or computable procedure that was equivalent to the consistency of a formal theory was discovered by Kurt Gödel's incompleteness theorem, which is notable for a form of meta-mathematical encoding of the statement that "T can prove statement S" (the provability predicate) which is used in all these machines. This was further clarified by Alan Turing and Alonzo Church's work on a formal definition of computability.

Although not a traditional turing machine, in 2012 Merlin Carl and Boris Z. Moroz constructed a [[Diophantine Equation]] which had solutions if and only if NBG (Von Neumann–Bernays–Gödel set theory) is inconsistent. NBG is a conservative extension of ZFC, so solving this equation is independent of ZFC.<ref>Carl, M., & Moroz, B. Z. (2012). ''On a Diophantine representation of the predicate of provability.'' Zapiski Nauchnykh Seminarov POMI, 407, 77-104. (Republished in 2014 in the Journal of Mathematical Sciences) [https://webdoc.sub.gwdg.de/ebook/serien/e/mpi_mathematik/2006/129.pdf (preprint)]</ref>

There is no one authoritative source on the history of TMs independent of ZF, this is our best understanding of the history of TMs found. Mostly these are taken from Scott Aaronson's blog announcements and Busy Beaver Frontier or self-reported by the individuals who discovered them. The Aaronson-Yedida machine used a compiler called ''Laconic'', which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.

Note that only the results with a linked formal verification are known to have such a verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.
{| class="wikitable"
|+History of ZF independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|7910
|May 2016
|Adam Yedidia and Scott Aaronson
|Yedidia and Aaronson 2016<ref>A. Yedidia and S. Aaronson. A relatively small Turing machine whose behavior is independent of set theory. Complex Systems, (25):4, 2016. https://arxiv.org/abs/1605.04343</ref>
|
|-
|1919
|15 May 2016
|Stefan O'Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2016-zf-sorear-1919/zf.nql Github NQL file], [https://groups.google.com/g/metamath/c/OumBq83Ksqs/m/FogyOlLIBwAJ Metamath Group Announcement]
|
|-
|748
|May 2016
|Stefan O’Rear
|[https://github.com/sorear/metamath-turing-machines/blob/master/machines/2017-zf-sorear-748/zf2.nql Github NQL], Busy Beaver Frontier<ref name=":0" />
|
|-
|745
|July 2023
|Johannes Riebel
|Riebel 2023 Bachelor Thesis<ref>Riebel, Johannes (March 2023). ''[https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf The Undecidability of BB(748): Understanding Gödel's Incompleteness Theorems]'' (PDF) (Bachelor's thesis). University of Augsburg.</ref>
|
|-
|643
|July 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL], [https://scottaaronson.blog/?p=8131 Aaronson Announcement]
|
|-
|636
|31 August 2024
|Rohan Ridenour
|[https://github.com/CatsAreFluffy/metamath-turing-machines Github NQL] ([https://github.com/CatsAreFluffy/metamath-turing-machines/commit/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1 commit])
|
|-
|588
|12 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/30d2e3194866615f68dd2f5101cb300fb039adca commit])
|
|-
|549
|16 July 2025
|Andrew J. Wade
|[https://github.com/andrew-j-wade/metamath-turing-machines Github NQL] ([https://github.com/andrew-j-wade/metamath-turing-machines/commit/5d676aec074a94f598959cb3b7733a8f7781762f commit])
|
|-
|432
|19 Aug 2025
|Andrew J. Wade
|[https://codeberg.org/ajwade/turing_machine_explorer/commit/33b30300054242201a95679aacf7e74312bd8803b0df9a85d2314095efd6804e git commit]
|
|-
|335
|11 Oct 2026
|Jeff Ketchersid
|[https://discord.com/channels/960643023006490684/1331570843829932063/1559077555158392844 discord message]
|
|-
|254
|13 Oct 2026
|[https://x.com/_mira___mira_ Mira] with use of ChatGPT, formalized by [https://github.com/jeff87654 Jeff Ketchersid] with Claude
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Github]
|[https://github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m254 Rocq file]
|-
|230
|19 Oct 2026
|[https://x.com/ElliotGlazer Elliot Glazer] with use of ChatGPT, formalized with GPT and Claude
|[https://github.com/elliotglazer/k230-rocq Github]
|[https://github.com/elliotglazer/k230-rocq Rocq file]
|-
|215
|21 Oct 2026
|[[wikipedia:Cleo_(mathematician)|Vladimir Reshetnikov]] formalized with Claude
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal Github]
|[https://github.com/VladimirReshetnikov/ProveIt/tree/c9dc79323429112c698100f3226a6e4d56c8b782/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 Rocq file]
|}
[[File:ZFC Machine 254.png|thumb|The transition table of the machine with 254 states. The initial state is 1.]]
Wade's 432-state champion also omits the [[wikipedia:Axiom_of_regularity|axiom of regularity]], as ZF-regularity is also equiconsistent with ZF.

For Peano Arithmetic, the ZF independent machines are an upper bound. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower [[wikipedia:Equiconsistency#Consistency_strength|consistency strength]]. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(PA).

{| class="wikitable"
|+History of Peano Arithmetic (PA) independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|372
|11 February 2026
|@LegionMammal978 (Matthew House)
|[https://github.com/LegionMammal978/turing_machine_explorer/blob/main/pa.py Github]
|
|}
This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.<ref>https://mathoverflow.net/questions/508137/interpreting-pa-with-only-adjunction-separation/508161</ref>

== New Foundations (NF) ==

A November 2026 research development gives a 210-working-state, two-symbol Turing machine designed to halt exactly when a fixed first-order presentation of Quine's New Foundations (NF) has a contradiction proof. The archive contains an external Lean 4.35.0 formalization and a source-only verification package.

Under the assumption that NF is syntactically consistent, the development derives that NF cannot prove a specified numerical upper bound on the ''runtime'' function BB(210), or its exact numerical value. Under the stronger assumption of arithmetic Σ₁-soundness of NF, the true exact-value equation is neither provable nor refutable in NF. The numerical value is not computed. This differs from results about ZF or PA; it does not give a 210-state independence bound for those theories.

The source files and past verification receipts are published at [https://github.com/wlad-svennik/notes/tree/main/nf-bb210 GitHub]. The original machine has 210 working states, 420 binary transition rows, and SHA-256 <code>129fc1fe44f609c18c2dfbc6df367835bbee7d6a02bbda3480b93d3c2c52646a</code>. The statement is formalized as an ''external'' Lean metatheorem rather than a completed PA-internal derivation. As of this publication, a fresh independent clean build and community review have not been reported.

=== Large cardinals ===
These tables are for theories stronger than ZFC.

{| class="wikitable"
|+History of ZFC + "There exist arbitrarily large subtle cardinals" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|493
|25 February 2026
|@LegionMammal978
|[https://github.com/Saoi2/turing_machine_explorer/blob/main/subtle.tm Github]
|
|}
This machine takes Wade's ZF champion and adds the [[wikipedia:Axiom_of_choice|axiom of Choice]] and a statement from Harvey Friedman (Proposition 4.3 of [https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf "Primitive Independence Results"])<ref>H. Friedman, "[https://bpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/PrimitiveIndResults071302-189vmn0.pdf Primitive Independence Results]" (2002). Accessed February 2026.</ref> which Friedman showed to be equivalent to "There exist arbitrarily large subtle cardinals" over ZFC.

For reference, this theory is between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the [[wikipedia:Large_cardinal|large cardinal hierarchy]] on Wikipedia.

Note: The initial machine produced in 2016 by Yedidia and Aaronson is designed to halt iff a certain statement created by Harvey Friedman is true.<ref name=":0" /> According to Friedman (without a published proof), this statement is independent of the theory "Stationary Ramsey Property" or ''SRP'', which is equiconsistent with the theory <math>ZFC + \{\text{``There is a }k\text{-subtle cardinal``}\mid k\in\N\}</math> which is also between the strength of "strongly unfoldable" and "<math>0^\sharp</math> exists" on the large cardinal hierarchy.<ref>tlonuqbar, "[https://mathoverflow.net/questions/508364/what-is-the-consistency-strength-of-srp-stationary-ramsey-property What is the consistency strength of SRP (Stationary Ramsey Property)?]" (2026). MathOverflow post, accessed February 2026.</ref> However, the theory used by the BB(493) machine is also independent of this theory.

{| class="wikitable"
|+History of ZF + "There exists a Berkeley cardinal" independent TMs
!States
!Date
!Discoverer
!Source
!Verification
|-
|1399
|8 November 2026
|@Meganeuridae
|[https://github.com/Meganeuridae/large-cardinal-tms/blob/main/berkeley-rocq/machine/machine.tm Github]
|[https://github.com/Meganeuridae/large-cardinal-tms/tree/main/berkeley-rocq/coq/Berkeley Rocq file]
|}

Berkeley cardinals are perhaps the strongest family of large cardinals considered, initially proposed by Hugh Woodin at a lecture at UC Berkeley as an axiom that was "obviously inconsistent".{{Citation needed}} However, no inconsistency has been found and many people now believe it may be consistent. Berkeley cardinals are known to be inconsistent with the axiom of choice.

== Footnotes ==
<references group="footnote"/>

== References ==
<references />

[[Category:Zoology]]