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.

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]
• 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.^[19]
  • On October 12, cppdecksucker claimed to have used Aristotle AI to prove Ξ₀_SK(8) = 80.^[20]
• Domain-Restricted Instruction-Limited Busy Beaver
  • On October 10, star claimed to have used Claude, discovered a new champion for BBi(10, 6, 2) (colloquially known as BB(5.5)).^[21]
  • On October 11, star claimed to have used using Claude, reduced BBi(10, 6, 2) to 4 holdouts,^[22] all of which are present in the most recent holdouts equivalence list (BB6_holdouts_1581_eqv_740.txt).^[23] She believes that two of these holdouts (1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (bbch) and another equivalent machine) are Cryptids.^[24]
• Pebble Automaton
  • On October 13, AlephSquirrel proved peBBle(5) = 11 and peBBle(6) = 17.^[25]

Misc

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

Champions

• Jeff Ketchersid claimed to have used Claude Opus 5.5 to discover a set of small Ackermann-level champions, created by modifying the current BB(7) champion, including:
  • On October 4, a new BB(8) champion, 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_1LC0RH_1RG1LF (bbch), which takes over $2{\uparrow }^{37}3$ steps to halt. Prior to this, the BB(7) champion, found by Pavel Kropitz, which ran for around $2{\uparrow }^{11}2{\uparrow }^{11}3$ steps, held the BB(8) championship by default.^[27]
  • On October 7, a new BB(9) champion, 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_1RG1LD_0RH0RF_0RG0RE_0LH1RZ (bbch), which takes over $f_{\omega }(2{\uparrow }^{13}3)$ steps to halt.^[28] Prior to this, the BB(9) champion, found by Jacobzheng, ran for around$f_{\omega }(f_9(2))$ steps.
  • On October 8, a new BB(10) champion, 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC (bbch), which takes over $f_{\omega +1}(2{\uparrow }^{36}3)$ steps to halt.^[29] Prior to this, 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₆₄.

Holdouts

• 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.^[30]
  • 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.^[31]
  • On the same day, Andrew Ducharme released an unofficial holdout list of 37 machines.^[32]
• 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!
• 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.^[33]
  • On October 3, oscar claimed to have used GPT-6.1 Sol to prove a machine halting,^[34] formalized in Rocq the next day.^[35]
  • On October 6, Discord user Zuck claimed to have used Claude to prove a machine non-halting.^[36]
  • On October 7, mxdys released a holdout list of 778 machines up to equivalence.^[37]
  • On October 10, Discord user Dennis claimed to have used Claude Opus 5.5 to prove a machine non-halting.^[38]
  • On the same day, mxdys released a holdout list of 740 machines up to equivalence.^[39]
  • On October 11, Dennis claimed to have used Claude Opus 5.5 to prove another 4 machines non-halting.^[40]
  • On October 13, Dennis claimed to have used Claude Opus 5.5 to prove another 3 machines non-halting.^[41]
  • On the same day, Dennis claimed to have used Claude Opus 5.5 to prove a machine halting.^[42]
  • On October 15, mxdys released a holdout list of 698 machines up to equivalence.^[43]

Misc

• Logical Independence
  • On October 6, .mira.mira. (Twitter user @_Mira___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.^[44] 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.^[45]
  • On October 13, Jeff Ketchersid claimed to have used Claude Opus 5.5 to find a 335-state, 2-symbol TM, proven to halt if and only if ZFC is inconsistent, based on an earlier (previously unverified) 393-state machine discovered by Andrew Wade with the same property.^[46]