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).
BB Adjacent
General Recursive Functions: TODO: Further progress
- 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]
- BBµ(16) ≥ 47, found by Shawn on 5 May:
- 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 .[7] aparker[8] and star[9] proved that there is no such n.
- On 5 May, Shawn implemented a size 133 GRF that halts iff there was a counter-example to Fermat's Last Theorem: fermat.mgrf.[10]
- 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]
- Many new champions were discovered for the Busy Beaver variants of SKI calculus, SK calculus and BCKW system.
- On 1 May, discord user sheep discovered a BBCS(65) champion beating Graham's number.[12] On 3 May, sheep improved this champion to size 64.[13]
- BBCS(10) was shown to be exactly 16.[14]
- On 6 May, sheep discovered a new champion for BBCS(21)[15] and on 11 May a new champion for BBCS(25).[16]
- On 16 May, Azerty enumerated BBCS(11). [TODO: bug found, may have to be removed][17]
- On 28 May, @-d began enumerating BBf(23).[18] The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.[19]
TODO: Check for other BB-like functions' progress
Misc
- mxdys made his inductive decider for history-linear machines compilable into an executable file.[20]
- TODO: BB Bignum Bakeoff
- TODO: GPU deciders
Holdouts
| 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(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.[21]
- 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.[22][23]
- Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to 501,914[24][25], then to 439,120 again using the inductive decider.[26] 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]