TMBR: May 2026

Prev: April 2026

This Month in Beaver Research

Next: June 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 May 2026.

BB Adjacent

General Recursive Functions:

• Some new champions were found:
  • BBµ(16) ≥ 47, found by Shawn on 5 May: M(C(R(S, R(P(2,1), R(P(3,2), C(R(S, P(3,1)), P(5,3), P(5,2))))), P(1,1), S)).^[1]
  • BBµ(17) ≥ 2090, found by Shawn on 8 May: M(C(R(P(1,1),R(P(2,1),R(R(R(S,C(S,P(3,2))),P(4,1)),P(5,2)))),P(1,1),S)).^[2]
  • BBµ(93) ≥ Graham's number, designed by racheline on 19 May using a binary encoding of weak goodstein sequences.^[3][4]
• Some new cryptids were hand-built:
  • Size 56, by Shawn on 2 May (simulating 5x+1 problem starting at 7).^[5]
  • Size 49, by aparker, star and Shawn on 3 May (simulating Brocard's problem).^[6]
• The first non-trivial divergent GRF was found (size 15). It halts iff there exists some n ≥ 1 such that n+3 divides $Tetr(n)=\frac{n(n+1)(n+2)}{6}$.^[7] aparker^[8] and star^[9] proved that there is no such n.
• On 5 May, Shawn implemented a size 133 GRF that non-trivially halts iff there is a counter-example to Fermat's Last Theorem: fermat.mgrf.^[10] Note that since Fermat's Last Theorem is true, this GRF does not halt; however, this GRF is still of interest due to the complexity of the proof of the theorem.
• On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S).^[11]
• All M(PRF) GRFs were decided up to size 12 with max score 5.^[12]
• All PRFs were decided up to size 22 with max score $\approx 2^{2^{230}}$. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.^[13]

SKI Calculus:

• On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,^[14] and some small champions for Ξ₀_SK(n) for sizes 9 to 15.^[15]
• By 7 May, an unknown person translated 2014MELO03's lambda calculus champion to SKI calculus, proving the bound Ξ₀(25) > Graham's number^[16] (falsely attributed to 2014MELO03).
• On 15 May, Δ⁵ proved the bound Ξ₀(22) > Graham's number.^[17]
• On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀_SK(6) = 10.^[18]
• On 22 May, Δ⁵ discovered smaller tetrational (size 13) and pentational (size 17) terms in the SKI calculus, and 50_ft_locker proved the bound Ξ₀(20) > Graham's number.^[19]
• On 23 May, Boone discovered new Ξ₀_SK(n) champions for sizes 7 to 12^[20] (and Ξ₀(n) champions for sizes 7 to 10^[21]), as well as a Ξ₀(11) champion 2 days later.^[22]
• On 25 May, Azerty introduced the Busy Beaver function for the BCKW system.^[23]
• On 26 May, Δ⁵ discovered some tetrational (size 7) and Ackeramnn-growth (size 11) terms in the BCKW system, and proved the bound Ξ₀_BCKW(12) > Graham's number.^[24]
• On 29 May, Δ⁵ discovered an infinite family of terms in the SKI calculus with normal form growth rate f_ω⋅2(n).^[25]

CounterScript:

• On 1 May, discord user sheep discovered a BBCS(65) champion beating Graham's number.^[26] On 3 May, sheep improved this champion to size 64.^[27]
• On 6 May, sheep discovered a new champion for BBCS(21)^[28] and on 11 May a new champion for BBCS(25).^[29]
• On 13 May, sheep proved CounterScript Turing-complete via a translation from B*olfuck to Counterscript.^[30] 2 days later, she showed that CounterScript restricted to 3 registers was also Turing-complete.^[31]
• On 23 May, Azerty enumerated BBCS(11).^[32] All 39 holdouts were shown to be non-halting, proving BBCS(11) = 20.^[33][34]

Fractran:

• On 28 May, @-d began enumerating BBf(23).^[35] The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.^[36]

TODO: Check for other BB-like functions' progress

Misc

• mxdys made his inductive decider for history-linear machines compilable into an executable file.^[37]
• TODO: BB Bignum Bakeoff
• TODO: GPU deciders
• LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating axiomatically undecidable machines.^[38]

Holdouts

BB Holdout Reduction by Domain

Domain	Previous Holdout Count	New Holdout Count	Holdout Reduction	% Reduction
BB(4,3)	5,641,006	5,127,263	513,743	9.11%
BB(3,4)	12,049,358	11,362,197	687,161	5.70%
BB(2,5)	66	65	1	1.52%
BB(2,6)	536,112	413,513	122,599	22.87%

• BB(7)
  • David SG begins directly simulating the 17.8 million BB(7) holdouts using one of their servers, simulating over 1 million holdouts to halting.^[39]

• BB(2,5)
  • Andrew Ducharme found a FAR solution for a machine, which previously had an informal nonhalting argument. On June 1st, mxdys provided the Rocq proof, reducing the Rocq-holdout count to 65.
• BB(4,3)
  • Andrew Ducharme reduced the number of holdouts from 5,641,006 to 5,127,263, a 9.11% reduction, with mxdys's new inductive decider.^[40]
• BB(3,4)
  • XnoobSpeakable completed Stage 2 of Phase 3, reducing to number of holdouts from 12,049,358 to 11,362,197, a 5.70% reduction.
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 536,112 to 527,232 via Enumerate.py and TM-enum, a 1.66% reduction.^[41][42]
  • Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to 501,914^[43][44], then to 439,120 again using the inductive decider.^[45] In total this was a 16.71% reduction.
  • Using FAR, Andrew Ducharme further reduced the number of holdouts from 439,120 to 418,127, a 4.78% reduction.
  • Using some mxdys deciders, Andrew Ducharme continued reducing the number of holdouts through May 17, from 418,127 to 413,513 (a 1.10% reduction).^{[13][14][15][16]}
• BB(2,7)
  • Terry Ligocki enumerated 130K more subtasks, increasing the number of holdouts to 1,087,732,936. A total of 350K subtasks out of the 1 million subtasks (or 35%) have been enumerated.^[17]