TMBR: July 2026: Difference between revisions
Jump to navigation
Jump to search
m formatting |
→BB Adjacent: Wnagtlies |
||
| Line 18: | Line 18: | ||
TODO: Post Tag System | TODO: Post Tag System | ||
* [[Wang Tiles]] | |||
** Over July 22-25, AlephSquirrel found champions 1-4 and proved their optimality, and found the BB_WT(5) champion. | |||
** Prior work by Emmanuel Jeandel and Michael Rao in 2015 shows BB_WT(10) ≥ 212.<ref>https://arxiv.org/abs/1506.06492</ref> | |||
== Holdouts == | == Holdouts == | ||
Revision as of 15:44, 3 October 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
- A new champion was discovered for Ξ₀(12).
- New champions were discovered for Ξ₀SK(12), Ξ₀SK(13), Ξ₀S(14), Ξ₀SK(15), Ξ₀SK(16) and Ξ₀SK(17).
TODO: update
- 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
- Wang Tiles
- Over July 22-25, AlephSquirrel found champions 1-4 and proved their optimality, and found the BB_WT(5) champion.
- Prior work by Emmanuel Jeandel and Michael Rao in 2015 shows BB_WT(10) ≥ 212.[1]
Holdouts
| 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)
- 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.