TMBR: October 2026

Prev: September 2026

This Month in Beaver Research

Next: November 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 October 2026.

Blog Posts

• Blanking Beavers: Results and Open Problems. Nick Drozd. 20 Oct 2026.

BB Adjacent

• Register Machine
  • On October 1, sheep discovered a 12-state, 2-register Cryptid which halts iff 7 converges to 1 under the Collatz-like 5n+1 map, thus showing that MBB(12, 2) is hard.^[1]
  • On the same day, @-d enumerated MBB(8), which left 7,891 holdouts after reduction, or 404 holdouts if an ai-created decider is used.^[2]
  • On the same day, @mineralli discovered a family of champions for MBB(n, 1).^[3]
  • On October 2, @mineralli discovered a new champion for MBB(10, 2).^[4]
  • On the same day, sheep discovered 2 new tetrational champions for MBB(10).^[5][6]
  • On the same day, Shawn Ligocki released an MBB(8) holdout list consisting of 145 holdouts,^[7] using another ai-created decider similar to CTL.^[8]
  • On October 3, Shawn Ligocki released another MBB(8) holdout list consisting of 46 holdouts,^[9] later reduced to 6^[10] (from 7^[11]) holdouts.
  • On the same day, Shawn Ligocki discovered a cryptid similar to Space Needle amongst the 6 remaining holdouts, showing MBB(8) is hard.^[12]
  • On the same day, sheep analyzed the rest of the holdouts, discovering 4 equivalences and another Space Needle-like cryptid (Needle 1),^[13] meaning MBB(8) "probviously" = 3,394.
  • On the same day, Katelyn Doucette devised a method to show that a sizeable portion of powers of two could not be reached by Needle 1's path.^[14] She later concluded that this backwards reasoning-like method, though powerful, would not be enough to decide Needle 1.^[15]
  • On October 7, sheep rediscovered a 2003 dissertation by Rick Griffiths^[16] which investigated the (maximum register value) Busy Beaver function for register machines (Beaver(n)); Griffiths determines the values of Beaver(n) for sizes 1 to 4 (using the modern instruction counting convention), and provides lower bounds for sizes 5 to 8. It also provides a machine (constructed by Ortwin Gasper in 2003) which shows the bound MBB(11) > 10↑↑17.74.^[17]
  • On October 8, sheep marginally improved the bounds for MBB(10).^[18]
  • On October 10, AlephSquirrel rediscovered a 2020 article by Yuri Matiyasevich^[19] which provides a 130-instruction, 29-register machine which halts if and only if the Riemann hypothesis is false.^[20]
  • On October 17, mineralli published a script capable of converting any arbitrary register machine into an equivalent 2-register machine.^[21]
• SKI Calculus
  • On October 8, cppdecksucker shared a holdouts list for Ξ₀_SK(8) consisting of 17 terms, 2 of which have been decided to not have a normal form.^[22]
  • On October 12, cppdecksucker claimed to have used Aristotle AI to prove Ξ₀_SK(8) = 80.^[23]
  • On the same day, Δ⁵ proved Ξ₀_BCKW(5) = 47.^[24]
  • On October 13, Δ⁵ translated a 15 combinator term in the BCKW calculus, demonstrating Ξ₀_BCKW(15) > $f_{{\omega }^{2\uparrow \uparrow 18-1}}(2)$.^[25]
• Lambda Calculus
  • On October 9, Discord user Sam discovered a new 80 bit term,^[26] shown by 50_ft_lock to demonstrate the bound BBλ(80) > $f_{{\omega }^{\omega }+1}(3)$.^[27]
  • On October 13, Sam optimized the BBλ(80) champion to a reduced and improved 79 bit term, demonstrating the bound BBλ(79) > $f_{{\omega }^{\omega }+1}(7)$.^[28]
  • On the same day, Gustavo Melo estimated that a specific family of terms, mentioned earlier by Sam,^[29] reaches $f_{{\omega }^{\omega }\cdot 2+1}$ growth.^[30]
  • On the same day, Sam discovered new $f_{{\omega }^{\omega }\cdot 2+1}$-level champions for BBλ(70), BBλ(74), BBλ(78), and BBλ(80).^[31]
  • On October 15, Gustavo Melo discovered new $f_{{\omega }^{{\omega }^{\omega }}}$-level champions for BBλ(77),^[32] BBλ(80),^[33] and BBλ(85) (the next day),^[34] and conjectured that a specific 76 bit term would have a normal form greater than $f_{{\omega }^{{\omega }^3}}(2)$ bits.^[35]
  • On October 16, Δ⁵ discovered a new 80 bit term, demonstrating the bound BBλ(80) > $f_{{\omega }^{{\omega }^{14}}}(2)$.^[36][37]
  • On the same day, Gustavo Melo proved the conjecture about the 76 bit term's size, demonstrating the bound BBλ(76) > $f_{{\omega }^{{\omega }^3}}(2)$.^[38]
• Domain-Restricted Instruction-Limited Busy Beaver
  • On October 10, star claimed to have used Claude to discover a new champion for BBi(10, 6, 2) (colloquially known as BB(5.5)).^[39]
  • On October 11, star claimed to have used Claude to reduce BBi(10, 6, 2) to 4 holdouts,^[40] all of which are present in the most recent holdouts equivalence list (BB6_holdouts_1581_eqv_740.txt).^[41] She believes that two of these holdouts (1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (bbch) and another equivalent machine) are Cryptids.^[42]
• Fractran
  • On October 13, @-d completed the verification of the ai-generated 1dpc decider and its certificates, reducing the official count of BBf(23) holdouts from 21,233 to 8,021, and the official count of BBf(24) holdouts from 231,432 to 85,726.^[43]
  • On the same day, @-d discovered 0.1% of certificates created by the ai-generated ndpc decider to be invalid, hypothesized to have been caused by a soundness bug in the decider.^[44]
• Pebble Automaton
  • On October 13, AlephSquirrel proved peBBle(5) = 11 and peBBle(6) = 17.^[45]
  • On October 18, AlephSquirrel proved peBBle(7) = 28.^[46]
  • On October 19, Shawn Ligocki claimed to have used Google Gemini to prove peBBle(8) = 63 using a CTL-like method,^[47] and to find 54,394 9-pebble holdouts (including automata with multiple undefined transitions),^[48] later reduced to 376 holdouts,^[49] then 104 holdouts,^[50] before claiming to have proven peBBle(9) = 63,577.^[51]
  • On October 20, Shawn Ligocki claimed to have used Google Gemini to find 1,867 10-pebble holdouts (including automata with multiple undefined transitions),^[52] later reduced to 1,221 holdouts.^[53]

Champions

New BB(n, 2) champions discovered this month

n	BB(n)			BB(n) prior to October
	Champion	Discoverer	Lower bound	Discoverer	Lower bound
8	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_1LC0RH_1RG1LF (bbch)	Jeff Ketchersid	$2{\uparrow }^{37}3$	Pavel Kropitz	$2{\uparrow }^{11}2{\uparrow }^{11}3$
9	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_1RG1LD_0RH0RF_0RG0RE_0LH1RZ (bbch)		$f_{\omega }(f_9(2))$	Jacobzheng	$f_{\omega }(f_9(2))$
10	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC (bbch)		$f_{\omega }^2(25)>g_{64}$	racheline	$f_{\omega }^2(25)$
12	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RK0LC_0RL---_0RF1RZ (bbch)		$f_{\omega +1}(f_{\omega +1}(2{\uparrow }^{37}3))$		$>f_{\omega }^4(2\uparrow \uparrow \uparrow 4-3)>f_{\omega }^4(f_4(2))$
13	1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_0LG1RI_1RE0RH_1LF0RC_1RM0LE_1LA1LE_0LL1LB_0RM1LL_1RZ1RH (bbch)		$f_{\omega +2}(f_{\omega }(20))$	50_ft_lock	$>f_{\omega +1}(2046)>g_{64}$
14	1RB1RA_1RI1RC_0LD1LG_0RE1LD_1LN1RF_1LJ0RA_1RA0LH_1LG1LH_1RK0LM_1RZ0LE_0LE0RJ_1LH1LM_0LH0LL_0LG1LN (bbch)		$f_{\omega +2}^3(15)$	Jacobzheng	$>f_{\omega +1}(f_{\omega }^4(f_7(3)))$

• Jeff Ketchersid claimed to have used Claude Opus 5.5 to discover and prove the scores of a set of Ackermann-level machines, four of which (BB(8),^[54] BB(9),^[55] BB(10),^[56] BB(12)^[57]) were derived from the current BB(7) champion, and two of which (BB(13), BB(14))^[58] were derived from Jacobzheng's former champion for BB(14), specifically:
  • On October 4, a new BB(8) champion, which takes over $2{\uparrow }^{37}3$ steps to halt. Prior to October, the BB(7) champion, found by Pavel Kropitz, which held the BB(8) championship by default, ran for around $2{\uparrow }^{11}2{\uparrow }^{11}3$ steps.
  • On October 7, a new BB(9) champion, which takes over $f_{\omega }(2{\uparrow }^{13}3)$ steps to halt. Prior to October, the BB(9) champion, found by Jacobzheng, ran for around$f_{\omega }(f_9(2))$ steps.
  • On October 8, a new BB(10) champion, which takes over $f_{\omega +1}(2{\uparrow }^{36}3)$ steps to halt. Prior to October, the BB(10) champion, found by racheline, ran for around $f_{\omega }^2(25)$ steps. This is also the smallest 2-symbol machine (in states) known to run for longer than a Graham's number number number of steps; in other words, this machine shows that BB(10) > g₆₄, improving on 50_ft_lock's earlier result that BB(13) > g₆₄.
  • On October 14, a new BB(12) champion, which takes over $f_{\omega +1}(f_{\omega +1}(2{\uparrow }^{37}3))$ steps to halt. Prior to October, the BB(12) champion, found by racheline, ran for around $f_{\omega }^4(2\uparrow \uparrow \uparrow 4-3)$ steps.
  • On the same day, a new BB(13) champion, which takes over $f_{\omega +2}(f_{\omega }(20))$ steps to halt. Prior to October, the BB(13) champion, found by 50_ft_lock, ran for around $f_{\omega +1}(2046)$ steps.
  • On the same day, a new BB(14) champion, which takes over $f_{\omega +2}^3(15)$ to halt. Prior to October, the BB(14) champion, found by Jacobzheng, ran for around $f_{\omega +1}(f_{\omega }^4(f_7(3)))$ steps.

Holdouts

BB Holdout Reduction by Domain

Domain	New Holdout Count	Previous Holdout Count	Holdout Reduction	% Reduction
BB(6)	663	797	134	16.81%
BB(4,3)	4,719,315	4,720,332	1,017	0.02%
BB(2,5)	37	39	2	5.13%
BB(2,6)	393,659	412,086	18,427	4.47%
BB(2,7)	3,125,433,611	Enumeration incomplete	N/A	N/A

TODO: update BB holdout reduction by domain, since there will probably be a new holdout list by the end of the week.

• BB(6)
  • On October 1, Discord user oscar claimed to have used GPT-6.1 Sol to prove a machine non-halting, formalized in Rocq the next day.^[59]
  • On October 1, dyuan shared a subset of BB(6) holdouts, consisting of 24 machines which are expected to be easily analyzable by longitudinal analysis.^[60]
  • On October 3, oscar claimed to have used GPT-6.1 Sol to prove a machine halting,^[61] formalized in Rocq the next day.^[62]
  • On October 6, Discord user Zuck claimed to have used Claude to prove a machine non-halting.^[63]
  • On October 7, mxdys released a holdout list of 778 machines up to equivalence.^[64]
  • On October 10, Discord user Dennis claimed to have used Claude Opus 5.5 to prove a machine non-halting.^[65]
  • On the same day, mxdys released a holdout list of 740 machines up to equivalence.^[66]
  • On October 11, Dennis claimed to have used Claude Opus 5.5 to prove another 4 machines non-halting.^[67]
  • On October 13, Dennis claimed to have used Claude Opus 5.5 to prove another 3 machines non-halting.^[68]
  • On the same day, Dennis claimed to have used Claude Opus 5.5 to prove a machine halting.^[69]
  • On October 15, mxdys released a holdout list of 698 machines up to equivalence.^[70]
  • On the same day, research entity Google DeepMind claimed to have used Gemini 3.1 Pro to discover and prove simple rules that characterise the behavior of 11 holdouts, noting them as potential Cryptids.^[71]
  • On the same day, Google DeepMind claimed to have used Gemini 3.1 Pro to prove 7 machines halting, and another 20 machines (pull requests #1, #2, #3, #4) non-halting.^[72]
  • On the same day, Dennis claimed to have used Claude Opus 5.5 and GPT-6 Astra to prove another 8 machines (pull requests #1, #2, #3, #4, #5) non-halting.^[73]
  • On October 16, mxdys released a holdout list of 663 machines up to equivalence.^[74]
  • On the same day, Re-us claimed to have used Claude Opus 5.5 to discover 7 probviously halting machines (described as energy vampires) which rely on an exceedingly rare tape configuration to halt, similar to the mechanism used by 1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA (bbch).^[75][76] Over the following few days, Re-us, Andrew Ducharme, and Ersen would continue to simulate 3 of the unique orbits (equivalent to 5 machines), confirming four of the machines do not halt within 10 billion rule applications.^{[77][78][79][80]} Re-us has also estimated that, assuming perfect randomness of the machines' bit generation, a median of 780 billion rule applications would have to be applied for each machine to halt.^[81][82]
  • On October 18, Ersen claimed to have used Claude to help run an independent (and currently ongoing) run of Antihydra to 2³⁸ rule applications, seemingly verifying apgoucher's results.^[83][84]
• BB(4,3)
  • Andrew Ducharme reduced the number of holdouts from 4,720,332 to 4,719,315, a 0.02% reduction, by using enumerate.py.^[85]
• BB(2,5)
  • On October 2, prurq claimed to have used Aristotle AI, to prove one of the remaining holdouts halting, reducing the unofficial count to 38 out of initially 60 Rocq-proven.^[86]
  • On October 9, prurq simulated a machine to halting using a Rocq-certified program, reducing the official and unofficial counts to respectively 59 and 37.^[87]
  • On the same day, Andrew Ducharme released an unofficial holdout list of 37 machines.^[88]
  • On October 17, LegionMammal978 simulated 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch) to over 10^{1,140,000,000} steps,^[89] previously claiming the machine to be a doubly-exponential probviously halting "hard-drive vampire".
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 412,086 to 393,659, a 4.47% reduction.^[90][91]
• BB(2,7)
  • Terry Ligocki enumerated 20K more subtasks, increasing the number of holdouts to 3,125,433,611. All 1 million subtasks have been enumerated! This enumeration took from November 2025 to October 2026 using the resources [Ligocki] had available to work on this enumeration. Now we can start decreasing the number of holdouts!

Misc

• On October 9, Google DeepMind claimed to have used Gemini 3.1 Pro to discover a 24-state, 2-symbol TM, proven to halt if and only if Goldbach's conjecture is false, improving on the previous smallest known machine with this property by one state.^[92]
• On October 10, Google DeepMind claimed to have used Gemini 3.1 Pro to formalize (Riemann, ZFC) the claims of Shunia's 120-state, 2-symbol TM's halting if and only if the Riemann Hypothesis is false, and the independence of Wade's 393-state, 2-symbol TM's halting status in ZFC.^[93]
• On October 13, Google DeepMind claimed to have used Gemini 3.1 Pro to reduce the number of states required for a specific 2-symbol TM to encode the truth value of the Goldbach conjecture from 25 to 21,^[94] the Riemann hypothesis from 120 to 104,^[95] and the consistency of ZFC from 393 to 380.^[96]
• On October 18, Discord user charlie claimed to have used Claude to reduce the number of states required for a specific 2-symbol TM to encode the truth value of the Weak Collatz conjecture from 124 to 23.^[97]
• On October 19, Google DeepMind claimed to have used Gemini 3.1 Pro to reduce the number of states required for a specific 2-symbol TM to encode the truth value of the Riemann hypothesis from 104 to 95.^[98]
• On October 20, Mira claimed to have used GPT-6 Astra^[99] to reduce the number of states required for a specific 2-symbol TM to encode the truth value of the Weak Collatz conjecture from 23 to 16.^[100][101]

This month, Mira, using GPT-6 Astra, has claimed to have found this 254-state, 2-symbol Turing machine that halts if, and only if, ZFC is inconsistent (Jeff Ketchersid has claimed to have proven this property using Claude Opus 5.5). The transition table of Mira's machine is shown in this image, with state 1 corresponding to the starting state.

• Logical Independence
  • On October 6, Mira claimed to have used GPT-6 Astra to reduce their previous 256-state, 2-symbol TM whose halting status is independent of ZFC, to a 254-state TM.^[102] They estimate that the Metamath formalization verifying that their previous 238-state, 2-symbol TM is independent of Peano Arithmetic is roughly 70% complete, and the formalization verifying that their new 254-state TM is independent of ZFC is roughly 40% complete.^[103]
  • On October 13, Jeff Ketchersid claimed to have used Claude Opus 5.5 to discover a 335-state, 2-symbol TM, proven to halt if and only if ZFC is inconsistent, based on an earlier 393-state machine discovered by Andrew Wade with the same property.^[104]
  • On October 14, Jeff Ketchersid claimed to have used Claude Opus 5.5 to prove the independence of Mira's 254-state TM's halting status from ZFC.^[105]
  • On October 15, Mira claimed to have used GPT-6 Astra to prove the independence of their 238-state TM's halting status from PA, building off of Jeff Ketchersid's proof of their ZFC-independent TM.^[106]
  • On October 18, Vladimir Reshetnikov claimed to have used Claude to reduce Mira's previous 254-state, 2-symbol TM whose halting status is independent of ZFC, to a 246-state TM.^[107][108]
  • On October 19, Kinata claimed to have used GPT-6 Astra^[109] to reduce Reshetnikov's previous 246-state, 2-symbol TM whose halting status is independent of ZFC, to a 230-state TM.^[110][111]