TMBR: November 2025

Prev: October 2025

This Month in Beaver Research

Next: December 2025

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

Talks

• Tristan Stérin gave a talk about bbchallenge and the BB(5) proof at Collège de France: Le cinquième nombre Busy Beaver (in French).^[1]
• Carl Kadie gave a talk on BB during the PyData Seattle 2025 conference: How to make Python programs run very slow (and new Turing Machine results).^[2]
• (From June) Terence Tao mentioned bbchallenge in their talk "The Equational Theories Project: advancing collaborative mathematical research at scale" (video / slides) at the 2025 Big Proof workshop. The talk is from June, but was just shared on the bbchallenge Discord this month.^[3] The talk is about the Equational Theories Project, a large-scale mathematical collaboration that crowd-sourced a proof in Lean. Tao mentions bbchallenge as the only other example of a large-scale mathematical collaboration to prove a single result that he knows of.

Themed Months

There have been two specific BB domain themed months: BB(3,3) month (October) and BB(2,5) month (November). For BB(3,3), this resulted in the clarification of some of the results and techniques on the Discord and Wiki. LegionMammal wrote up a detailed explanation of the probvious halter. No further progress on holdouts was made in October due to the limited number of holdouts and the work that's already been put into trying to solve them. For BB(2,5), it was verified that the Wiki was up to date. @mxdys shared some of his old notes on the unanalyzed machines.

Optimization

Benchmark for vonhust's simulator run on BB(6) holdouts.

Discord user vonhust created a fast TM simulator that averages 2 billion steps / s. It uses fixed-block Macro Machines with each block bit-packed into integers. It is about 10x faster than direct simulators across most TMs.^[4]

BB Adjacent

All Fractran deciders summarized and their relations, shared by Daniel Yuan on 14 Nov 2025

• Busy Beaver for Fractan (BBf) was introduced on 1 Nov by Jason Yuen.^[5] Exact values have been proven up to BBf(19) = 370 and exhaustive enumeration has been run up to size 21 (with BBf(21) ≥ 31,957,632 and 587 holdouts). No Cryptids have been found yet by enumeration, but Hydra has been encoded into a size 29 fractran program, so this provides a sort of upper bound on solvability.
• Cyclic Tree Busy Beaver (CTBB) was introduced by Discord user Jack on 14 Nov.^[6] The exact value is known for CTBB(2) = 5 and lower bounds have been found up to size 7 with CTBB(7) > 4↑↑↑↑(4↑↑↑3).
• Quite a few other BB variants have been proposed this month, but don't seem to have been significantly explored yet: BB110 (for Rule 110), BB_trw, BB_cgol (for Conway's Game of Life), Tiny Tag and Busy Beaver for SKI calculus.
• The Bashicu Matrix System milestone for BBλ has been reduced from 350 to 331.^[7]

Holdouts

• BB(6): Total holdout reduction: 204 TMs, a 12% reduction!
  • @mxdys released a holdouts list consisting of 1534 machines up to equivalence, which is a 6% reduction (84 machines)
  • @mxdys decided a holdout from 50 Random Holdouts by hand, making 11/50 solved. He also decided 5 more machines with a single strategy. (This machine was solved before the holdouts list, and as such, is not in it).
  • At the end of the month, @mxdys released a holdouts list consisting of only 1416 holdout TMs. A total of 118 holdouts were solved. 88 by a new FAR method, created by mxdys. 30 more by 14 new individual proofs by mxdys and 16 informal proofs verified.
  • A new holdouts list was created by Robin Rovenszky via searching the Discord server for any results on TMs. This spreadsheet thus includes every informal result alongside verified results.
  • Right after, Peacemaker decided a TM by hand. @mxdys verified this result using an Inductive decider.
  • With substantial work, a machine was formally proven nonhalting by Pomme, Autumn Pan, vyx and mxdys. However, this result is yet to be verified.
• BB(2,7): Enumeration started!
  • The code provided by mxdys breaks up the BB(2,7) enumeration into 1 million subtasks which each run for ~10 minutes and leave ~2500 holdouts based on an average of the first 1K subtasks. These values are about 5 times longer than and 25 times larger than the ones for BB(7).
  • Terry Ligocki enumerated the first 40K subtasks, resulting in 124,025,546 holdouts, which can be found here.
  • The expected number of holdouts after the enumeration is ~3B TMs.