TMBR: October 2026: Difference between revisions
Jump to navigation
Jump to search
Qwertyasdf (talk | contribs) No edit summary |
update |
||
| Line 1: | Line 1: | ||
{{TMBRnav|September 2026|November 2026}} | {{TMBRnav|September 2026|November 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).'' [[:Category:This Month in Beaver Research|This Month in Beaver Research]] for October 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).'' | ||
[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for October 2026. | |||
== BB Adjacent == | == BB Adjacent == | ||
* On 1 | * [[Register machine|Register Machine]] | ||
* On the same day, @-d enumerated MBB(8), which left 7,891 holdouts after reduction, or 404 holdouts if an ai-created decider is used.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555102010473193513]</sup> | ** On October 1, sheep discovered a 12-state, 2-register [[Cryptid]] which halts iff 7 converges to 1 under the Collatz-like 5n+1 map, thus showing that MBB(12, 2) is hard.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555083694937604097]</sup> | ||
* On the same day, @mineralli discovered a family of champions for MBB(n, 1).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555268332465422508]</sup> | ** On the same day, @-d enumerated MBB(8), which left 7,891 holdouts after reduction, or 404 holdouts if an ai-created decider is used.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555102010473193513]</sup> | ||
* On 2 | ** On the same day, @mineralli discovered a family of champions for MBB(n, 1).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555268332465422508]</sup> | ||
* On the same day, sheep discovered 2 new tetrational champions for MBB(10).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555512334846402573][https://discord.com/channels/960643023006490684/1552294888740098139/1555546324567335048]</sup> | ** On October 2, @mineralli discovered a new champion for MBB(10, 2).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555502006372663337]</sup> | ||
* On the same day, Shawn Ligocki released an MBB(8) holdout list consisting of 145 holdouts,<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555699448066342953]</sup> using another ai-created decider similar to CTL.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555699290285019147]</sup> | ** On the same day, sheep discovered 2 new tetrational champions for MBB(10).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555512334846402573][https://discord.com/channels/960643023006490684/1552294888740098139/1555546324567335048]</sup> | ||
* On 3 | ** On the same day, Shawn Ligocki released an MBB(8) holdout list consisting of 145 holdouts,<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555699448066342953]</sup> using another ai-created decider similar to CTL.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555699290285019147]</sup> | ||
* On the same day, Shawn Ligocki discovered a cryptid amongst the 6 remaining holdouts, showing MBB(8) is hard.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555767330531967099]</sup> | ** On October 3, Shawn Ligocki released another MBB(8) holdout list consisting of 46 holdouts,<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555754019606106212]</sup> later reduced to 6<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555772428997886004]</sup> (from 7<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555759004444270633]</sup>) holdouts. | ||
* On the same day, sheep analyzed the rest of the holdouts, discovering 4 equivalences and another cryptid,<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555897664078618675]</sup> meaning MBB(8) "probviously" = 3,394. | ** On the same day, Shawn Ligocki discovered a cryptid similar to [[Space Needle]] amongst the 6 remaining holdouts, showing MBB(8) is hard.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555767330531967099]</sup> | ||
** On the same day, sheep analyzed the rest of the holdouts, discovering 4 equivalences and another Space Needle-like cryptid (Needle 1),<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1555897664078618675]</sup> meaning MBB(8) "probviously" = 3,394. | |||
** On the same day, Katelyn Doucette devised a method to show that a sizeable portion of powers of two could not be reached by Needle 1's path.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1556086800861233154]</sup> She later concluded that this backwards reasoning-like method, though powerful, would not be enough to decide Needle 1.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1556810508160606243]</sup> | |||
** On October 7, sheep rediscovered a 2003 [https://web.archive.org/web/20061216201733/http://www2.cantabgold.net/users/m.y.becker.98/part2projects/rickdissertation.zip dissertation] by Rick Griffiths<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1557447684896464909]</sup> which investigated the (maximum register value) Busy Beaver function for register machines (Beaver(n)); Griffiths determines the values of Beaver(n) for sizes 1 to 4 (using the modern instruction counting convention), and provides lower bounds for sizes 5 to 8. It also provides a machine (constructed by Ortwin Gasper in 2003) which shows the bound MBB(11) > 10↑↑17.74.<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1557623496044183603]</sup> | |||
** On October 8, sheep marginally improved the bounds for MBB(10).<sup>[https://discord.com/channels/960643023006490684/1552294888740098139/1557714856960983131]</sup> | |||
* [[SKI Calculus]] | |||
** On October 8, cppdecksucker shared a holdouts list for Ξ₀<sub>SK</sub>(8) consisting of 17 terms, 2 of which have been decided to not have a normal form.<sup>[https://discord.com/channels/960643023006490684/1552337976946597928/1557759102187348009]</sup> | |||
* [[Instruction-Limited Busy Beaver|Domain-Restricted Instruction-Limited Busy Beaver]] | |||
** On October 10, star, using Claude, discovered a new champion for BBi(10, 6, 2) (colloquially known as BB(5.5)).<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558608094949416993]</sup> | |||
** On October 11, star, using Claude, reduced BBi(10, 6, 2) to 4 holdouts,<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558654629821157499]</sup> all of which are present in the most recent holdouts equivalence list (BB6_holdouts_1581_eqv_740.txt).<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558671475999772775]</sup> She believes that two of these holdouts ({{TM|1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF|halt}} and another equivalent machine) are Cryptids.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558766480424964169]</sup> | |||
== Misc == | == Misc == | ||
* On 1 | * On October 1, dyuan shared a subset of [[BB(6)]] holdouts, consisting of 24 machines which are expected to be easily analyzable by [[Longitudinal Analysis|longitudinal analysis]].<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1555244959840337973]</sup> | ||
== Champions == | == Champions == | ||
* Jeff Ketchersid | * Jeff Ketchersid discovered a set of small Ackermann-level champions, created by modifying the current [[BB(7)]] champion, including: | ||
* On October 4, a new [[BB(8)]] [[champion]], {{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_1LC0RH_1RG1LF|halt}}, which takes over <math>2 \uparrow^{37} 3</math> steps to halt. Prior to this, the [[BB(7)]] champion, found by Pavel Kropitz, held the BB(8) championship by default.<sup>[https://discord.com/channels/960643023006490684/1448375857046360094/1556422395776995408]</sup> | |||
* On October 7, a new BB(9) champion, {{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_1RG1LD_0RH0RF_0RG0RE_0LH1RZ|halt}}, which takes over <math>f_{\omega}(2 \uparrow^{13} 3)</math> steps to halt.<sup>[https://discord.com/channels/960643023006490684/1331570843829932063/1557495370014130300]</sup> Prior to this, the BB(9) champion, found by Jacobzheng, ran for just over <math>f_{\omega}(f_{9}(2))</math> steps. | |||
* On October 8, a new BB(10) champion, {{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC|halt}}, which takes over <math>f_{\omega + 1}(2 \uparrow^{36} 3)</math> steps to halt.<sup>[https://discord.com/channels/960643023006490684/1331570843829932063/1557806386073702622]</sup> Prior to this, the BB(10) champion, found by racheline, ran for just over <math>f_{\omega}^2(25)</math> steps. This is also the smallest 2-symbol machine (in states) known to run for longer than a [[Graham's number]] number number of steps; in other words, this machine shows that BB(10) > g<sub>64</sub>, improving on 50_ft_lock's earlier result that BB(13) > g<sub>64</sub>. | |||
== Holdouts == | == Holdouts == | ||
* [[BB(2,5)]] | * [[BB(2,5)]] | ||
**On October 2, prurq claimed to have | **On October 2, prurq, using Aristotle AI, claimed to have to proven one of the remaining holdouts halting, reducing the unofficial count to 38 out of initially 60 Rocq-proven.<sup>[https://discord.com/channels/960643023006490684/1259770421046411285/1555690509245087827]</sup> | ||
**On October 9, prurq simulated a machine to halting, reducing the unofficial count to 37.<sup>[https://discord.com/channels/960643023006490684/1259770421046411285/1558226290509742082]</sup> | |||
**On the same day, Andrew Ducharme released an unofficial holdout list of '''37''' machines.<sup>[https://discord.com/channels/960643023006490684/1259770421046411285/1558248567800336394]</sup> | |||
*[[BB(2,7)]] | *[[BB(2,7)]] | ||
** Terry Ligocki enumerated 20K more subtasks, increasing the number of holdouts to '''3,125,433,611'''. All 1 million subtasks have been enumerated! This enumeration took from November 2025 to October 2026 using the resources | ** Terry Ligocki enumerated 20K more subtasks, increasing the number of holdouts to '''3,125,433,611'''. All 1 million subtasks have been enumerated! This enumeration took from November 2025 to October 2026 using the resources [Ligocki] had available to work on this enumeration. Now we can start decreasing the number of holdouts! | ||
*[[BB(6)]] | *[[BB(6)]] | ||
**On October 7, mxdys released | **On October 1, Discord user oscar proved a machine non-halting, [https://github.com/oscar172772/bb6-1RB1RF_1LC0LF_---0LD_0LE1LD_0RF0LB_1RA1RE-nonhalt-proof formalized] in Rocq the next day.<sup>[https://discord.com/channels/960643023006490684/1555183165977403453/1555641766391324813]</sup> | ||
**On October 3, oscar proved a machine halting,<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1555992557148831755]</sup> formalized in Rocq the next day.<sup>[https://discord.com/channels/960643023006490684/1556006145649545247/1556258332048887889]</sup> | |||
**On October 6, Discord user Zuck proved a machine non-halting.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1557025952217833632]</sup> | |||
**On October 7, mxdys released a holdout list of '''778''' machines up to equivalence.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1557353710101995550]</sup> | |||
**On October 10, Discord user Dennis [https://github.com/DennisKoshta/busycoq/blob/59de13796aa9dbccedd52bc5d081e87980dd2f7e/verify/BellEatsCounter_1RB0RF.v proved] a machine non-halting.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558558131213041755]</sup> | |||
**On the same day, mxdys released a holdout list of '''740''' machines up to equivalence.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558585686288891986]</sup> | |||
**On October 11, Dennis proved another 4 machines non-halting.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1558644008199262220]</sup> | |||
[[Category:This Month in Beaver Research|2026-10]] | [[Category:This Month in Beaver Research|2026-10]] | ||
Revision as of 15:26, 11 October 2026
| Prev: September 2026 | This Month in Beaver Research | Next: November 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).
This Month in Beaver Research for October 2026.
BB Adjacent
- Register Machine
- On October 1, sheep discovered a 12-state, 2-register Cryptid which halts iff 7 converges to 1 under the Collatz-like 5n+1 map, thus showing that MBB(12, 2) is hard.[1]
- On the same day, @-d enumerated MBB(8), which left 7,891 holdouts after reduction, or 404 holdouts if an ai-created decider is used.[2]
- On the same day, @mineralli discovered a family of champions for MBB(n, 1).[3]
- On October 2, @mineralli discovered a new champion for MBB(10, 2).[4]
- On the same day, sheep discovered 2 new tetrational champions for MBB(10).[5][6]
- On the same day, Shawn Ligocki released an MBB(8) holdout list consisting of 145 holdouts,[7] using another ai-created decider similar to CTL.[8]
- On October 3, Shawn Ligocki released another MBB(8) holdout list consisting of 46 holdouts,[9] later reduced to 6[10] (from 7[11]) holdouts.
- On the same day, Shawn Ligocki discovered a cryptid similar to Space Needle amongst the 6 remaining holdouts, showing MBB(8) is hard.[12]
- On the same day, sheep analyzed the rest of the holdouts, discovering 4 equivalences and another Space Needle-like cryptid (Needle 1),[13] meaning MBB(8) "probviously" = 3,394.
- On the same day, Katelyn Doucette devised a method to show that a sizeable portion of powers of two could not be reached by Needle 1's path.[14] She later concluded that this backwards reasoning-like method, though powerful, would not be enough to decide Needle 1.[15]
- On October 7, sheep rediscovered a 2003 dissertation by Rick Griffiths[16] which investigated the (maximum register value) Busy Beaver function for register machines (Beaver(n)); Griffiths determines the values of Beaver(n) for sizes 1 to 4 (using the modern instruction counting convention), and provides lower bounds for sizes 5 to 8. It also provides a machine (constructed by Ortwin Gasper in 2003) which shows the bound MBB(11) > 10↑↑17.74.[17]
- On October 8, sheep marginally improved the bounds for MBB(10).[18]
- SKI Calculus
- On October 8, cppdecksucker shared a holdouts list for Ξ₀SK(8) consisting of 17 terms, 2 of which have been decided to not have a normal form.[19]
- Domain-Restricted Instruction-Limited Busy Beaver
- On October 10, star, using Claude, discovered a new champion for BBi(10, 6, 2) (colloquially known as BB(5.5)).[20]
- On October 11, star, using Claude, reduced BBi(10, 6, 2) to 4 holdouts,[21] all of which are present in the most recent holdouts equivalence list (BB6_holdouts_1581_eqv_740.txt).[22] She believes that two of these holdouts (
1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF(bbch) and another equivalent machine) are Cryptids.[23]
Misc
- On October 1, dyuan shared a subset of BB(6) holdouts, consisting of 24 machines which are expected to be easily analyzable by longitudinal analysis.[24]
Champions
- Jeff Ketchersid discovered a set of small Ackermann-level champions, created by modifying the current BB(7) champion, including:
- On October 4, a new BB(8) champion,
1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_1LC0RH_1RG1LF(bbch), which takes over steps to halt. Prior to this, the BB(7) champion, found by Pavel Kropitz, held the BB(8) championship by default.[25] - On October 7, a new BB(9) champion,
1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_1RG1LD_0RH0RF_0RG0RE_0LH1RZ(bbch), which takes over steps to halt.[26] Prior to this, the BB(9) champion, found by Jacobzheng, ran for just over steps. - On October 8, a new BB(10) champion,
1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC(bbch), which takes over steps to halt.[27] Prior to this, the BB(10) champion, found by racheline, ran for just over steps. This is also the smallest 2-symbol machine (in states) known to run for longer than a Graham's number number number of steps; in other words, this machine shows that BB(10) > g64, improving on 50_ft_lock's earlier result that BB(13) > g64.
Holdouts
- BB(2,5)
- On October 2, prurq, using Aristotle AI, claimed to have to proven one of the remaining holdouts halting, reducing the unofficial count to 38 out of initially 60 Rocq-proven.[28]
- On October 9, prurq simulated a machine to halting, reducing the unofficial count to 37.[29]
- On the same day, Andrew Ducharme released an unofficial holdout list of 37 machines.[30]
- BB(2,7)
- Terry Ligocki enumerated 20K more subtasks, increasing the number of holdouts to 3,125,433,611. All 1 million subtasks have been enumerated! This enumeration took from November 2025 to October 2026 using the resources [Ligocki] had available to work on this enumeration. Now we can start decreasing the number of holdouts!
- BB(6)
- On October 1, Discord user oscar proved a machine non-halting, formalized in Rocq the next day.[31]
- On October 3, oscar proved a machine halting,[32] formalized in Rocq the next day.[33]
- On October 6, Discord user Zuck proved a machine non-halting.[34]
- On October 7, mxdys released a holdout list of 778 machines up to equivalence.[35]
- On October 10, Discord user Dennis proved a machine non-halting.[36]
- On the same day, mxdys released a holdout list of 740 machines up to equivalence.[37]
- On October 11, Dennis proved another 4 machines non-halting.[38]