TMBR: April 2026

Prev: March 2026

This Month in Beaver Research

Next: May 2026

This Month in Beaver Research for April 2026. This month, a new Cryptid was discovered in BB(6) by Discord user sheep, and BMO 8 was added to the Beaver Math Olympiad. Two informally proven machines were formalised into Rocq in BB(2,5). There was a 40% reduction in BB(4,3), and we also passed below 18 million holdouts for BB(7). There's been a lot of discoveries in the Fractran, General Recursive Function, and Lambda Calculus versions of Busy Beaver. Katelyn Doucette created a visualizer for Fractran space-time diagrams. BBf(22) has been solved except for the Fenrir family of Cryptids. The first BBµ champion was found that takes advantage of the minimization (M) operator. Both BBf(100) and BBµ(100) were proven to surpass Graham's number. BBλ(38) was solved and a 74-bit BBλ Cryptid was found.

BB Adjacent

Space-time diagram of Space Needle in Fractran.

• Fractran
  • BBf(22) was solved with the exception of the Fenrir family. Enumeration of BBf(23) would take roughly 10 days.^[1]
  • Katelyn Doucette created a visualizer for Fractran space-time diagrams.
  • Racheline created a series of fast-growing programs: a tetrational program of size 29,^[2] $f_{\omega }$ programs starting from size 86,^[3] and $f_{\omega +1}$ programs from size 95, meaning Graham's number fits under size 100. She predicts that one probably exists under size 40, and that it shouldn't be hard to reduce it to at least 60.
  • BBf(n) was added to OEIS: A395424
• General Recursive Function
  • Jacob Mandelson proved the values up to BBµ(7) on 3 Apr.^[4]
  • A couple of Cryptids were hand-constructed: size 141, by Jacob on 8 Apr,^[5] and size 81, by Shawn Ligocki on 28 Apr.^[6]
  • Shawn built an "Ackermann worm" function with $f_{\omega }$ growth of size 83 on 16 Apr and used to it show BBµ(100) > Graham's number.^[7]
  • Jacob extended the Ackermann worm to find a $f_{{\omega }^2}$ growth function of size 204 on 23 Apr.^[8][9]
  • Shawn enumerated all Primitive Recursive Functions (GRF w/o Min) up to size 20.^[10][11][12]
  • Shawn found a series of new chaotic size 14 champions using the Min operator on 29 Apr, proving BBµ(14) ≥ 32.^[13] The longest running takes ~30k sim steps and all size 14 GRF of the form M(PRF) have been simulated out to 10M sim steps.^[14]
  • Shawn is working on a distributed computation version of GRF enumeration so that others can contribute compute.^[15]
• Busy Beaver for Lambda Calculus
  • BBλ(38) has been solved (BBλ(38) = $5\cdot 2^{2^{2^{2^2}}}+6$).
  • A Cryptid was found in 74 bits.
  • Tromp's BB Lambda paper got published in the journal Entropy.
• "BB" for Sokoban has been shared on the Discord server. (Although it is computable like Bug Game, so we wouldn't call it a BB-function.)
• Jumping Busy Beaver has been introduced, JBB(2,2,n) is known for n = 0 to n = 10, along with some lower bounds on small domains, see the Discord thread.

Misc

• ZTS439 explored some properties of summations over the Hydra function $S(n)=\sum _{k=0}^{n}H(k)$.^[16]

Holdouts

BB Holdout Reduction by Domain

Domain	Previous Holdout Count	New Holdout Count	Holdout Reduction	% Reduction
BB(6)	1161	1104	57	4.91%
BB(7)	18,036,852	17,823,260	213,592	1.18%
BB(4,3)	9,401,447	5,641,006	3,760,441	40.00%
BB(3,4)	12,435,284	12,049,358	385,926	3.10%
BB(2,5)	69	66	3	4.35%
BB(2,6)	545,005	536,112	11,241	1.63%

BB(6) progress in 2026 so far -- by mxdys

• BB(6): Reduction: 57. No. of TMs to simulate to 1e14: 161 (reduction: 10). To 1e15: 225 (reduction: 13).
  • Discord user sheep discovered^[17][18] a new Cryptid, 1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE (bbch), similar to Space Needle. A classification of Cryptids is now being worked on, where this machine, for example, could belong to a class of Needles (along with Space Needle).
  • BMO 8 was added to the Beaver Math Olympiad: 1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA (bbch)
  • The Turing Machine 1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB--- has been informally solved for months now. The formal solution depends on a number theory result which would be a major project in of itself to formalise. Therefore, the following statement was formalised: assuming the Baker–Wüstholz core bound for linear forms in logarithms over ℚ, the Turing machine never halts. See Github, Axiom minimal version: Discord, The machine's Discord thread: Link. Note that the formal proofs were made with the help of Claude Opus and Aristotle AI.
  • mxdys released a new holdouts list of 1119 machines, the reduction mostly (except for one TM, the other informal holdout) came from finding new equivalences. This means there is now only 1 holdout (see above) whose solution has not been fully formalised.
  • Later, mxdys released a new holdouts list of 1104 machines where more equivalence classes have been merged.
  • These equivalences were found with the help of -d, see (Discord 1, 2, 3). Equivalences seem to be amongst the last low-ish hanging fruits, with -d estimating about 100-200 equivalences left.
  • Alistaire and Discord user @The_Real_Fourious_Banana each simulated a TM to 1e15 steps. Combined with the recent equivalence reductions (10 machines total), the number of machines to simulate to 1e14 and 1e15 steps is 161 & 225 respectively.
• BB(7)
  • Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to 17,823,260.^[19] (A 1.18% reduction)
• BB(4,3):
  • In phase 2 stage 3, Andrew Ducharme reduced the number of holdouts from 9,401,447 to 5,641,006, a 40.00% reduction. He also found several new high-scoring halters, current places 4 through 8 in the 4x3 Busy Beaver game. 4th place is 1RB1LD2LA_0RC1RZ0RA_1LD2LA0LC_2RD2RC0LD (bbch) with approximate sigma score ~10↑↑1023.47221. ^[20]
• BB(3,4):
  • Andrew Ducharme began Phase 3, reducing the holdout count from 12,435,284 to 12,049,358 (a 3.10% reduction) with mxdys's FAR decider.
• BB(2,5):
  • On 1 April 2026, Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution, which he created using Aristotle AI. Then mxdys formalised the result in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.
  • On 2 April 2026, mxdys solved BMO 3 variant 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB (bbch) using an LLM, reducing the formal holdout count to 66. The proofs for BMO 3 and its variant are available at https://github.com/ccz181078/busycoq/blob/BB6/verify/BMO3.v.
  • 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch) and 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch) were simulated until halting by prurq using Quick_Sim.^[21][22] These TMs, in addition to 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch), were shown to halt in 2024 June (see Discord), but step counts and scores for these machines were unknown.
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 545,005 to 536,112 via Enumerate.py, a 1.63% reduction.^[23][24][25]
• BB(2,7)
  • Terry Ligocki enumerated 120K more subtasks, increasing the number of holdouts to 687,123,946. A total of 220K subtasks out of the 1 million subtasks (or 22%) have been enumerated. (see Google Drive) ^[26][27]