TMBR: July 2026: Difference between revisions
Jump to navigation
Jump to search
No edit summary |
m →Holdouts: Removed three colon to make the "Holdout" sections consistent with previous months. |
||
| Line 41: | Line 41: | ||
|0.77% | |0.77% | ||
|} | |} | ||
* [[BB(6)]] | * [[BB(6)]] | ||
** On 2 July, mxdys solved three holdouts in rocq.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1522010493529751604][https://discord.com/channels/960643023006490684/1239205785913790465/1522209150699044904]</sup> | ** On 2 July, mxdys solved three holdouts in rocq.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1522010493529751604][https://discord.com/channels/960643023006490684/1239205785913790465/1522209150699044904]</sup> | ||
** On 3 July, mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1522617640554860574 solved another holdout] in rocq using an LLM. | ** On 3 July, mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1522617640554860574 solved another holdout] in rocq using an LLM. | ||
| Line 47: | Line 47: | ||
** On 28 July, prurq [https://discord.com/channels/960643023006490684/1239205785913790465/1531564686238027976 found a TM to halt]. This was [https://discord.com/channels/960643023006490684/1239205785913790465/1532416648533901503 verified by mxdys] in rocq two days later together with another machine. | ** On 28 July, prurq [https://discord.com/channels/960643023006490684/1239205785913790465/1531564686238027976 found a TM to halt]. This was [https://discord.com/channels/960643023006490684/1239205785913790465/1532416648533901503 verified by mxdys] in rocq two days later together with another machine. | ||
** TODO: BMO 9 and BMO 10 | ** TODO: BMO 9 and BMO 10 | ||
* [[BB(4,3)]] | * [[BB(4,3)]] | ||
** Andrew Ducharme reduced the number of holdouts from 4,784,443 to '''4,747,566''', a '''0.77%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1522168741922607164][https://discord.com/channels/960643023006490684/1084047886494470185/1530496818155229294]</sup> | ** Andrew Ducharme reduced the number of holdouts from 4,784,443 to '''4,747,566''', a '''0.77%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1522168741922607164][https://discord.com/channels/960643023006490684/1084047886494470185/1530496818155229294]</sup> | ||
*[[BB(2,7)]] | *[[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. | **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. | ||
[[Category:This Month in Beaver Research|2026-07]] | [[Category:This Month in Beaver Research|2026-07]] | ||
Revision as of 00:43, 6 September 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), Ξ₀_SK(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
TODO: Wang tiles (https://discord.com/channels/960643023006490684/1529586687926210691)
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.