TMBR: July 2026

Prev: June 2026

This Month in Beaver Research

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

General

• Verification of BB(5) = 47,176,870 in Lean:
  • On July 14, Marcelo Fornet used Claude AI to translate the proof of BB(5) = 47,176,870 to Lean, save for two machines: Skelet #1, and Skelet #17.^[1]
  • On July 16, the non-halting proof for Skelet #17 was translated to Lean.^[2]
  • On July 25, the non-halting proof for Skelet #1 was translated to Lean, thus completing the proof of BB(5) = 47,176,870 in Lean.^[3]

BB Adjacent

• SKI Calculus:
  • Δ⁵ discovered several new champions for Ξ₀_SK(12),^[4], Ξ₀_SK(14),^[5] Ξ₀(12), Ξ₀_SK(15),^[6] and Ξ₀_SK(16).^[7]
  • On July 27, Δ⁵ discovered a new pentational champion for Ξ₀_BCKW(7) and new hexational champions for Ξ₀_BCKW(8) and Ξ₀_BCKW(9).^[8]
  • On the same day, Δ⁵ discovered a new pentational champion for Ξ₀_SK(22), and new hexational champions for Ξ₀_SK(23), Ξ₀_SK(24), and Ξ₀_SK(25).^[9]
  • On July 28, Δ⁵ discovered a new pentational champion for Ξ₀_SK(17).^[10]
• CounterScript:
  • On July 16, Azerty discovered a logical leap in a claimed equivalence,^[11] prompting another re-enumeration of BBCS(11), leaving the same 1 holdout.^[12] This holdout was previously proven non-halting by sheep on May 17,^[13] racheline on July 8,^[14] and Tobias B on July 11.^[15]
• General Recursive Function:
  • On July 16, Shawn Ligocki reduced the size 16 M(PRF) holdout list to 15 and proved those remaining 15 non-halting by hand, proving that the max value is 6.^[16] He shared what appears to be the hardest size 15 program which depends on logic for divisibility of triangular numbers.^[17]

• Lambda Calculus:
  • On July 20, BBλ(40) was solved, showing that BBλ(40) ≈ 10↑↑↑16. BBλ(40) is the first solved domain in any non-trivial BB variant to reach pentational values.

• Post Tag System
  • On July 21, Shawn Ligocki introduced the Busy Beaver function for Post Tag Systems, BB_PT(n),^[18] and provided champions for BB_PT(n) for sizes 7 to 11.^[19]
  • On the same day, Shawn Ligocki shared holdout lists for tag systems with sizes less than 12.^[20]
  • On July 22, Shawn Ligocki proved the values of BB_PT(n) for sizes 1 to 6, and shared a set of 9 holdouts with sizes less than 9.^[21]
  • On July 24, sheep discovered a supposedly "halting" tag system of size 11, with a mechanism similar to cryptids.^[22] However, after a careful simulation by Shawn Ligocki,^[23] it was realized that the system was an actual cryptid,^[24] showing BB_PT(11) is hard.

• Wang Tiles
  • On July 22, AlephSquirrel introduced the Busy Beaver function for Wang Tiles, BB_WT(n), and proved the values of BB_WT(1) and BB_WT(2).^[25]
  • On the same day, mathmasterzach established the lower bound BB_WT(n) ≥ n.^[26]
  • On July 23, sheep rediscovered literature^[27] from Emmanuel Jeandel and Michael Rao that implies BB_WT(10) ≥ 212, and is decidable.^[28]
  • On July 24, AlephSquirrel proved BB_WT(3) = 3.
  • On July 25, AlephSquirrel proved BB_WT(4) = 4.^[29]
  • On the same day, AlephSquirrel found a new BB_WT(5) champion.^[30]
  • On July 26, Shawn Ligocki noted that the behavior of the BB_WT(5) champion could be extended to establish the lower bound BB_WT(n) ≥ 2n - 4.^[31]

Holdouts

BB Holdout Reduction by Domain

Domain	Previous Holdout Count	New Holdout Count	Holdout Reduction	% Reduction
BB(6)	1,094	1,064	30	2.74%
BB(4,3)	4,784,443	4,747,566	36,877	0.77%

• BB(6)
  • On July 1, mxdys solved 4 holdouts in rocq.^[32][33]
  • On July 2, mxdys solved another holdout in rocq.^[34]
  • On July 3, mxdys solved another holdout in rocq with the help of an LLM.
  • On July 28, prurq found a TM to halt. This was verified by mxdys in rocq two days later together with another machine.
  • On the same day, mxdys released a new holdouts list of 1,064 machines up to equivalence, a 2.74% reduction compared to the previous holdouts list.
• BB(4,3)
  • Andrew Ducharme reduced the number of holdouts from 4,784,443 to 4,747,566, a 0.77% reduction.^[35][36]
• BB(2,5)
  • On July 30, prurq simulated a holdout to halting.^[37]
• BB(2,7)
  • Terry Ligocki enumerated 180K more subtasks, increasing the number of holdouts to 2,185,010,519. A total of 700K subtasks out of the 1 million subtasks (or 70%) have been enumerated.