TMBR: November 2026

Prev: October 2026

This Month in Beaver Research

Next: 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).

This Month in Beaver Research for November 2026.

Media

• YouTube video: 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

New champions discovered this month

Domain	Champion	Discoverer	New lower bound	Discoverer	Previous lower bound
BB(17)	1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO (bbch)	Jeff Ketchersid	$f_{\omega +3}^3(9)$
BB(18)	1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ (bbch)		$f_{\omega +3}^4(9)$	Jeff Ketchersid	$f_{\omega +3}(114)$
BB(19)	1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR (bbch)	User:Jacobzheng	$f_{\omega +7}^2(5)$
BB(20)	1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR (bbch)		$f_{\omega *2}(f_{\omega +2}^2(f_{10}(2)))$	User:Jacobzheng	$f_{\omega +6}^2(4)$
BB(11,4)	1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK (bbch)	User:Loader3229	$f_{\omega \cdot 2}(21)$		$f_{\omega +3}^2(4)$
BB(8,5)	2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH (bbch)		$f_{\omega \cdot 2+1}(93)$	User:Loader3229	$f_{\omega \cdot 2}(32)$
BB(4,6)	5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD (bbch)		$f_{\omega +2}(29)$		$f_{\omega +1}(2{\uparrow }^{15}5)$
BB(5,6)	1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE (bbch)		$f_{\omega +3}(31)$
BB(6,6)	4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB (bbch)		$f_{\omega *2}(89)$
BB(7,6)	2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG (bbch)		$f_{{\omega }^2}(63)$
BB(8,6)	0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG (bbch)		$f_{{\omega }^2+1}(7)$
BB(3,7)	6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC--- (bbch)		$f_{\omega +1}(77)$	User:Loader3229	$f_{\omega }^4(15)$
BB(4,7)	6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD--- (bbch)		$f_{\omega +2}(124)$

• 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) > $f_{\omega \cdot 2+1}(93)$.^[1] and BB(11,4) > $f_{\omega \cdot 2}(21)$.^[2]
  • On November 2, BB(4,6) > $f_{\omega +2}(29)$, BB(5,6) > $f_{\omega +3}(31)$, BB(6,6) > $f_{\omega \times 2}(36)$ and BB(7,6) > $f_{{\omega }^2}(28)$.
  • On November 3, BB(6,6) > $f_{\omega *2}(89)$.
  • On November 4, BB(7,6) > $f_{{\omega }^2}(63)$, BB(8,6) > $f_{{\omega }^2+1}(7)$, BB(3,7) > $f_{\omega +1}(77)$ and BB(4,7) > $f_{\omega +2}(124)$
• User:Jacobzheng discovered the following bounds:
  • On November 2, BB(20) > $f_{\omega +7}^2(5)$.
  • On November 4, BB(19) > $f_{\omega +7}^2(5)$ and BB(20) > $f_{\omega \times 2}(f_{\omega +2}^2(f_{10}(2))$.
• On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > $f_{\omega +3}(9)$, BB(18) > $f_{\omega +3}^4(9)$ and BB(19) > $f_{\omega +4}(f_{\omega +2}(114))$.

Holdouts

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.^[3]
• 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.^[4]

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 in the Wild (+ Energy Vampires)
  • Reus Vampires
    • On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts!^[5] This path corresponds to a group of machines with halting times of over 10^{683,718,950,000} steps, and decides the last of the 7 Reus vampires.

• Larger Cryptids
  • Logical Independence
    • Zermelo-Frankel set theory
      • On November 1, charlie claimed to have used Claude to formally reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
    • 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 announced 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.
• On November 4, Mira announced a Lean formalization of a 285-state P = NP beeper.
• On November 6, Mira released proofs for 284-state and 266-state NP = coNP beepers; the 284-state table is Lean-formalized, while the 266-state construction has a conventional proof.
• On November 9, GregoryMorse completed Lean formalizations for a suite of ten beepers, constructed with Claude assistance. These use designated beep states; Mira's headline counts use designated beep transitions.

Problem	Domain / convention	Discoverer	Date	Proof and notes
P = NP	285 states (beep transition)	Mira	November 4	Lean proof. Also proves the 286-state beep-state companion's equivalence.
NP = coNP	284 states (beep transition)	Mira	November 6	Lean proof for the marked table. A 285-state companion is documented separately.
NP = coNP	266 states (beep transition)	Mira	November 6	Conventional proof; no Lean literal-table theorem for this version. Its state-observer companion has 267 states.
P = NP	BBB(278) (beep state)	GregoryMorse, Claude	November 9	Lean machine proof and NP-completeness bridge.
P = PSPACE encoding	BBB(291) (beep state)	GregoryMorse, Claude	November 9	Lean proof: the encoded alternating-quantifier language belongs to P.
P = PP encoding	BBB(295) (beep state)	GregoryMorse, Claude	November 9	Lean proof: the encoded majority-acceptance language belongs to P.
NP = coNP encoding	BBB(317) (beep state)	GregoryMorse, Claude	November 9	Lean proof: a polynomially clocked nondeterministic guest recognizes the reference language's complement.
Integer factorization in P encoding	BBB(324) (beep state)	GregoryMorse, Claude	November 9	Lean proof: the bounded-divisor decision language belongs to P.
Discrete logarithms modulo primes in P encoding	BBB(400) (beep state)	GregoryMorse, Claude	November 9	Lean proof: the bounded-exponent decision language belongs to P.
Linear-time multiplication encoding	BBB(403) (beep state)	GregoryMorse, Claude	November 9	Lean proof: a linear-clocked multiplier exists in the queue-of-stacks guest model.
Graph isomorphism in P encoding	BBB(415) (beep state)	GregoryMorse, Claude	November 9	Lean proof: the encoded graph-isomorphism language belongs to P.
Linear-size NTT circuits encoding	BBB(469) (beep state)	GregoryMorse, Claude	November 9	Lean proof of the chain-circuit condition, assuming PrimeEx (prime existence).
Finitely many twin primes	BBB(19) (beep state)	GregoryMorse, Claude	November 9	Lean proof; beep state F. Reams's existing 18-state machine uses a beep transition.

Other problems encoded into Turing machines this month

Conjecture	Domain	Discoverer	Discovery date	Notes
Pillai's conjecture	BBBB(91)	charlie, Claude[6]	November 1	Unknown - pseudoquasihalts if the conjecture is false. Proof.