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

• TODO: BB(5) Lean proof completed: https://discord.com/channels/960643023006490684/1218877181321678928/1530515342772666429
• TODO: BBB(4) proof progress: https://discord.com/channels/960643023006490684/1385498968011575366/1532076512927420556

BB Adjacent

SKI Calculus:

• A new champion was discovered for Ξ₀(12).
• New champions were discovered for Ξ₀_SK(12), Ξ₀_SK(13), Ξ₀_SK(14), Ξ₀_SK(15), Ξ₀_SK(16) and Ξ₀_SK(17).

TODO: update

Lambda Calculus:

• BBλ(40) was solved on 20 July, showing that BBλ(40) ≈ 10↑↑↑16. BBλ(40) is the first solved domain in any BB variant to reach pentational values.

TODO: Post Tag System

TODO: Wang tiles (https://discord.com/channels/960643023006490684/1529586687926210691)

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 2 July, mxdys solved three holdouts in rocq.^[1][2]
  • On 3 July, mxdys solved another holdout in rocq using an LLM.
  • mxdys released a new holdouts list of 1,064 machines up to equivalence, this is a 2.74% reduction compared to the previous holdouts list.
  • On 28 July, prurq found a TM to halt. This was verified by mxdys in rocq two days later together with another machine.
  • TODO: BMO 9 and BMO 10
• BB(4,3):
  • Andrew Ducharme reduced the number of holdouts from 4,784,443 to 4,747,566, a 0.77% reduction.^[3][4]
• 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.