TMBR: June 2026

Prev: May 2026

This Month in Beaver Research

Next: July 2026

This Month in Beaver Research for June 2026. This month, Tristan presented the BB(5) paper at the ACM Symposium on Theory of Computing (STOC), BB(7) holdouts were reduced 11%, and several new champions were found across BB Adjacent models including BBλ(39) solved.

Talks

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

Papers

• William Gasarch. 2026. Relationships Between the Busy Beaver Function and Mathematics I: What is the Smallest n such that BB(n) > ...? SIGACT News 57, 2 (June 2026), 22–35. https://doi.org/10.1145/3819804.3819808

General

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

BB Adjacent

Busy Beaver for Lambda Calculus:

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

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)}[5], where q is a fast growing function arising from Laver tables. A day later, sheep showed that BBCS(89 + k) ≥ 2^Pk(0) where P(x) = q(x + 1).^[6]
• On 15 June, Shawn Ligocki discovered new champions for BBCS(13)^[7] and BBCS(14).^[8]
• On 20 June, sheep discovered two new champions (first, second) for BBCS(19) in quick succession, as well as new champions for BBCS(24) and BBCS(25).^[9]
• On 29 June, Azerty discovered multiple new bugs in the BBCS enumerator in quick succession,^[10] prompting a re-ennumeration of BBCS(11), leaving 51 holdouts.^[11]
• On 30 June, Azerty discovered more bugs in the BBCS enumerator,^[12] prompting another re-ennumeration of BBCS(11), leaving 51 holdouts again.^[13]

Fractran:

• On 1 June, Shawn Ligocki discovered a new BBf(23) champion which runs for over 4.393 × 10¹²⁴ steps.^[14]
• 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).^[15]
• MBB(6) = 49 was proven.

General Recursive Functions:

• On 23 June, Shawn Ligocki enumerated all PRF's of size 23^[16] and discovered a new champion PRF of size 23 with score $>10^{10^{130}}$.^[17]
• On 26 June, Shawn Ligocki discovered a new champion showing BBµ(17) ≥ 58,471.^[18]

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,^[19] 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.

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.^{[20][21][22][23]}
  • prurq solved another four TMs with FAR.^[24][25][26]
  • A TM was shown to be non-halting by hipparcos, which was later confirmed in Rocq by mxdys.
  • On 21 June, Peacemaker II solved another TM by running FAR with high parameters.
  • On 29 June, hipparcos showed another TM to be non-halting. This was verified in rocq by mxdys the same day.^[27]
  • 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 direct simulation, David SG reduced the number of remaining holdouts from 17,823,260 to 16,949,557, a 4.90% reduction.^[28]
  • Andrew Ducharme further reduced the amount of holdouts by 7.12% to 15,743,264 by running mxdys's FAR decider with various parameters.^[29]
• BB(4,3)
  • Andrew Ducharme reduced the number of holdouts from 5,127,263 to 4,784,443, a 6.69% reduction, using FAR.^[30][31][32]
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 413,513 to 412,086, a 0.35% reduction.^[33]
• 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.