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]
• Proof of BBB(4) = 32,779,478:
  • On July 29, @carrino used Claude AI to formally prove BBB(4) = 32,779,478, save for 290 holdouts, which do not appear in mxdys's holdout list.^[4]
  • On July 31, @carrino reduced the number of formal BBB(4) holdouts to less than 40.^[5]

BB Adjacent

• SKI Calculus:
  • On July 3, Δ⁵ discovered a new champion for Ξ₀_SK(12).^[6]
  • On July 10, Δ⁵ discovered new champions for Ξ₀(12) and Ξ₀_SK(14).^[7]
  • On July 19, Δ⁵ discovered new tetrational champions for Ξ₀(12), Ξ₀_SK(15), Ξ₀_SK(16), and Ξ₀_SK(17).^[8]
  • On July 27, Δ⁵ discovered a new pentational champion for Ξ₀_BCKW(7) and new hexational champions for Ξ₀_BCKW(8) and Ξ₀_BCKW(9).^[9]
  • On the same day, Δ⁵ tweaked the Ξ₀_SK(16) champion, improving the bound by roughly 33%.^[10]
  • On the same day, Δ⁵ discovered a new pentational champion for Ξ₀_SK(22), and new hexational champions for Ξ₀_SK(23), Ξ₀_SK(24), and Ξ₀_SK(25).^[11]
  • On July 28, Δ⁵ discovered a new pentational champion for Ξ₀_SK(17).^[12]
• CounterScript:
  • On July 16, Azerty discovered a logical leap in a claimed equivalence,^[13] prompting another re-enumeration of BBCS(11), leaving the same 1 holdout.^[14] This holdout was previously proven non-halting by sheep on May 17,^[15] racheline on July 8,^[16] and Tobias B on July 11.^[17]
• General Recursive Function:
  • On July 16, Shawn Ligocki found a size 13 version of a notable size 16 non-halting function which tested the divisibility of tetrahedral numbers.^[18]
  • On the same day, Shawn Ligocki proved that the largest number attained by a halting function of the form M(PRF) of size 13 is 6.^[19][20]

• 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),^[21] and provided champions for BB_WT(n) for sizes 7 to 11.^[22]
  • On the same day, Shawn Ligocki shared holdout lists for tag systems with sizes less than 12.^[23]
  • 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.^[24]
  • On July 24, sheep discovered a supposedly "halting" tag system of size 11, with a mechanism similar to cryptids.^[25] However, after a careful simulation by Shawn Ligocki,^[26] it was realized that the system was an actual cryptid,^[27] 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).^[28]
  • On the same day, mathmasterzach established the lower bound BB_WT(n) ≥ n.^[29]
  • On July 23, sheep rediscovered literature^[30] from Emmanuel Jeandel and Michael Rao that implies BB_WT(10) ≥ 212, and is decidable.^[31]
  • On July 24, AlephSquirrel proved BB_WT(3) = 3.
  • On July 25, AlephSquirrel proved BB_WT(4) = 4.^[32]
  • On the same day, AlephSquirrel found a new BB_WT(5) champion.^[33]
  • 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.^[34]

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.^[35][36]
  • On July 2, mxdys solved another holdout in rocq.^[37]
  • 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.^[38][39]
• BB(2,5)
  • On July 30, prurq simulated a holdout to halting.^[40]
• 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.