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:
- On July 3, Δ⁵ discovered a new champion for Ξ₀SK(12).[4]
- On July 10, Δ⁵ discovered new champions for Ξ₀(12) and Ξ₀SK(14).[5]
- On July 19, Δ⁵ discovered new tetrational champions for Ξ₀(12), Ξ₀SK(15), Ξ₀SK(16), and Ξ₀SK(17).[6]
- On July 27, Δ⁵ discovered a new pentational champion for Ξ₀BCKW(7) and new hexational champions for Ξ₀BCKW(8) and Ξ₀BCKW(9).[7]
- On the same day, Δ⁵ tweaked the Ξ₀SK(16) champion, improving the bound by roughly 33%.[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 found a size 13 version of a notable size 16 non-halting function which tested the divisibility of tetrahedral numbers.[16]
- 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.[17][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, BBPT(n),[19] and provided champions for BBPT(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 BBPT(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 BBPT(11) is hard.
- Wang Tiles
- On July 22, AlephSquirrel introduced the Busy Beaver function for Wang Tiles, BBWT(n), and proved the values of BBWT(1) and BBWT(2).[26]
- On the same day, mathmasterzach established the lower bound BBWT(n) ≥ n.[27]
- On July 23, sheep rediscovered literature[28] from Emmanuel Jeandel and Michael Rao that implies BBWT(10) ≥ 212, and is decidable.[29]
- On July 24, AlephSquirrel proved BBWT(3) = 3.
- On July 25, AlephSquirrel proved BBWT(4) = 4.[30]
- On the same day, AlephSquirrel found a new BBWT(5) champion.[31]
- On July 26, Shawn Ligocki noted that the behavior of the BBWT(5) champion could be extended to establish the lower bound BBWT(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.