TMBR: June 2026

Prev: May 2026

This Month in Beaver Research

Next: July 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).

Talks

• On 24 June, Tristan Stérin presented the BB(5) paper at STOC 2026 in Salt Lake City, USA.^[1]

BB Adjacent

Busy Beaver for Lambda Calculus:

• BBλ(39) was solved on 10 June, showing that BBλ(39) $=5\cdot 3^{3^{3^3}}+6$.
• Work began on BBλ(40), which was reduced to 2 holdouts^[2] and BBλ(41), which was reduced to 93 holdouts.
• A list of BBλ(42) holdouts was also added to the BBλ-spreadsheet.^[3]

SKI Calculus:

• New champions were discovered for Ξ₀(10), Ξ₀(13), Ξ₀(14), Ξ₀(15), Ξ₀(16), Ξ₀(17), Ξ₀(18) and Ξ₀(19).
• New SK calculus champions were discovered for Ξ₀_SK(18) and Ξ₀_SK(26), showing Ξ₀_SK(26) to be larger than Graham's number.
• New BCKW system champions were discovered for Ξ₀_BCKW(7), Ξ₀_BCKW(8) and Ξ₀_BCKW(9).

CounterScript:

• On 12 June, sheep constructed a size 85 champion with score $2^{q(5)}$^[4], where q is a fast growing function arising from Laver tables. A day later, sheep showed that BBCS(89 + k) $\ge 2^{P^k(0)}$ where P(x) = q(x + 1).^[5]
• On 15 June, Shawn Ligocki discovered new champions for BBCS(13)^[6] and BBCS(14).^[7]
• On the same day, Azerty completed the enumeration of BBCS(12), leaving an initial 866 holdouts.^[8] A second enumeration the next day left only 477 holdouts.^[9] [TODO: bug found, may have to be removed]
• On June 20, sheep discovered two new champions (first, second) for BBCS(19) in quick succession, as well as new champions for BBCS(24) and BBCS(25).^[10]

Fractran:

• On 1 June, Shawn Ligocki discovered a new BBf(23) champion which runs for over $4.393\times 10^{124}$ steps.^[11]
• BBf(23) holdouts were reduced by 27.20% from 29,250 to 21,295.

Register Machines:

• @-d discovered new champions for MBB(8) and MBB(9).^[12]
• MBB(6) was decided to be 49.

General Recursive Functions:

• Shawn Ligocki enumerated all PRF's of size 23.^[13]
• On 24 June Shawn Ligocki discovered a new champion PRF of size 23.^[14]
• On 25 June Shawn Ligocki discovered a new BBµ(19) champion.
• On 26 June Shawn Ligocki discovered two new BBµ(17) champions in quick succession.^[15][16]

Branching Beaver:

• Shawn Ligocki introduced the Branching Beaver (BrB(n,m)) function which is a variation of the Busy Beaver function, but where the tape is a graph where every node has 3 neighbors.
• Shawn computed exact values BrB(1) = 3 and BrB(2) = 10 and champions BrB(3) ≥ 52, BrB(4) ≥ 4636,^[17] BrB(2,3) ≥ 68, BrB(2,4) ≥ 332372. Enumeration sizes of BrB TMs is larger than for traditional BB TMs, so solving these values is expected to by harder than solving traditional BB.

Misc

• On 19 June, Marcelo Fornet shared a Lean formalization proving the BB(4) value.^[18] They are working on extending it to BB(5).
• TODO: GPU deciders

Holdouts

BB Holdout Reduction by Domain

Domain	Previous Holdout Count	New Holdout Count	Holdout Reduction	% Reduction
BB(6)	1,104	1,094	10	0.91%
BB(7)	17,823,260	15,743,264	2,079,996	11.67%
BB(4,3)	5,127,263	4,784,443	342,820	6.69%
BB(2,6)	413,513	412,086	1,427	0.35%

• BB(6)
  • mxdys solved four TMs with FAR.^{[19][20][21][22]}
  • prurq solved another four TMs with FAR.^[23][24][25]
  • A TM was shown to be non-halting by hipparcos, which was later confirmed in Rocq by mxdys.
  • On 21 May, Peacemaker II solved another TM by running FAR with high parameters.
  • On 29 May, hipparcos showed another TM to be non-halting. This was verified in rocq by mxdys the same day.^[26]
  • mxdys released a new holdouts list of 1,094 machines up to equivalence, this is a 0.91% reduction compared to the previous holdouts list.
• BB(7)
  • Using new GPU based deciders, David SG reduced the number of remaining holdouts from 17,823,260 to 16,949,557, a 4.90% reduction.^[27]
  • Andrew Ducharme further reduced the amount of holdouts by 7.12% to 15,743,264 by running mxdys's FAR decider with various parameters.^[28]
• BB(4,3):
  • Andrew Ducharme reduced the number of holdouts from 5,127,263 to 4,784,443, a 6.69% reduction, using FAR.^[29][30][31]
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 413,513 to 412,086, a 0.35% reduction.^[32]
• BB(2,7)
  • Terry Ligocki enumerated 170K more subtasks, increasing the number of holdouts to 1,623,113,079. A total of 520K subtasks out of the 1 million subtasks (or 52%) have been enumerated.