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]
• @carrino used Claude to begin work on proving the value of BBB(4) and formalizing the result in Rocq. On July 31, they were down to less than 40 holdouts.^[4]

BB Adjacent

• SKI Calculus:
  • Δ⁵ discovered several new champions for Ξ₀_SK(12),^[5], Ξ₀_SK(14),^[6] Ξ₀(12), Ξ₀_SK(15),^[7] and Ξ₀_SK(16).^[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, Δ⁵ discovered a new pentational champion for Ξ₀_SK(22), and new hexational champions for Ξ₀_SK(23), Ξ₀_SK(24), and Ξ₀_SK(25).^[10]
  • On July 28, Δ⁵ discovered a new pentational champion for Ξ₀_SK(17).^[11]
• CounterScript:
  • On July 16, Azerty discovered a logical leap in a claimed equivalence,^[12] prompting another re-enumeration of BBCS(11), leaving the same 1 holdout.^[13] This holdout was previously proven non-halting by sheep on May 17,^[14] racheline on July 8,^[15] and Tobias B on July 11.^[16]
• 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.^[17] He shared what appears to be the hardest size 15 program which depends on logic for divisibility of triangular numbers.^[18]

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

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