TMBR: May 2026
Jump to navigation
Jump to search
| 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
- 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] - 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 . All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.[13]
- 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.[14] On 3 May, sheep improved this champion to size 64.[15]
- BBCS(10) was shown to be exactly 16.[16]
- On 6 May, sheep discovered a new champion for BBCS(21)[17] and on 11 May a new champion for BBCS(25).[18]
- On 16 May, Azerty enumerated BBCS(11). [TODO: bug found, may have to be removed][19]
- On 28 May, @-d began enumerating BBf(23).[20] The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.[21]
TODO: Check for other BB-like functions' progress
Misc
- mxdys made his inductive decider for history-linear machines compilable into an executable file.[22]
- 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.[23]
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.[24]
- 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.[25][26]
- Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to 501,914[27][28], then to 439,120 again using the inductive decider.[29] 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]