TMBR: April 2026

Prev: March 2026

This Month in Beaver Research

Next: May 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 April 2026. This month, a new Cryptid was discovered in BB(6) by Discord user sheep, and BMO 8 was added to BMO. Two informally proven machines were formalised into Rocq in BB(2,5), and Katelyn Doucette created a visualizer for Fractran space-time diagrams. We also shot below 18 million holdouts for BB(7).

BB Adjacent

• General Recursive Function
  • 3 Apr: Jacob Mandelson proved the values up to BBµ(7).^[1]
  • 8 Apr: Jacob constructed a size 141 Cryptid.^[2]
  • 12 Apr: Shawn Ligocki enumerated all Primitive Recursive Functions (GRF w/o M) up to size 18, finding two new champions and guaranteeing that anything that beats them would have to use the Min operator.^[3][4]
  • 16 Apr: Shawn built a size 100 GRF that surpasses Graham's number.^[5]
  • 29 Apr: Shawn Ligocki found a new BBµ(14) champion using the min operator.^[6]
• "BB" for Sokoban has been shared on the Discord server. (Altough it is computable like Bug Game, so we wouldn't call it a BB-function.)
• Jumping Busy Beaver has been introduced, JBB(2,2,0) is known along with some lower bounds on small domains, see the Discord thread.
• 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: MDPI -- DOI

Misc

• Katelyn Doucette completed a visualizer for Fractran space-time diagrams.^[7]

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)
  • Discord user sheep discovered^[8][9] 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 result in Number Theory, which has not yet been formalised in any formal language, and doing so would be a large project. 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.
  • Alistaire simulated a machine to 1e15.
  • Discord user The_Real_Fourious_Banana simulated another TM to 1e15, reducing the 1e14 holdout count to 169 and the 1e15 holdout count to 235.
  • mxdys released a new holdouts list of 1119 machines, the reduction mostly (except for one TM, the other informal holdout) came from new equivalences. This means there is now only 1 holdout considered "informal", which is actually very formal, but depends on Baker's theorem (actually, more restricted than that is enough, see above), and therefore has not been fully formalised.
  • Later, mxdys released a new holdouts list of 1104 machines where more equivalence classes have been merged.
  • Along with the 1 TM simulated by Discord user @furiousbanana (Link to further simulation), the number of machines to simulate to 1e14 & 1e15 is X & Y respectively, due to the recent equivalence reductions. TODO: Add
  • TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034
• BB(7)
  • Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to 17,823,260.^[10] (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.^[11]
• 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^[12][13] which confirmed the already existing moderately formal argument further. 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch) is the only remaining machine suspected to halt from 2024 June, where the other two machines were first found to halt (see Discord).
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 545,005 to 536,112 via Enumerate.py, a 1.63% reduction.^[14][15][16]
• 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) ^[17][18]