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, BBPT(n),[18] and provided champions for BBPT(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 BBPT(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 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).[25]
- On the same day, mathmasterzach established the lower bound BBWT(n) ≥ n.[26]
- On July 23, sheep rediscovered literature[27] from Emmanuel Jeandel and Michael Rao that implies BBWT(10) ≥ 212, and is decidable.[28]
- On July 24, AlephSquirrel proved BBWT(3) = 3.
- On July 25, AlephSquirrel proved BBWT(4) = 4.[29]
- On the same day, AlephSquirrel found a new BBWT(5) champion.[30]
- 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.[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.