TMBR: May 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) m →Holdouts: Preassume reference |
Added BB(4,3) reduction |
||
| (5 intermediate revisions by 3 users not shown) | |||
| Line 2: | Line 2: | ||
''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 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).'' | ||
== BB Adjacent == | |||
[[General Recursive Function|General Recursive Functions]]: | |||
* Some new cryptids were hand-built: | |||
** Size 56, by Shawn on 2 May (simulating 5x+1 problem starting at 7).<sup>[https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/collatz.mgrf]</sup> | |||
** Size 49, by aparker, star and Shawn on 3 May (simulating [[wikipedia:Brocard's_problem|Brocard's problem]]).<sup>[https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/brocard.mgrf]</sup> | |||
* The first non-trivial divergent GRF was found (size 15). It halts iff there exists some n ≥ 1 such that n+3 divides <math>Tetr(n) = \frac{n(n+1)(n+2)}{6}</math>.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500584497542987776]</sup> aparker<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500587569514283098]</sup> and star<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500595210919346337]</sup> proved that there is no such n. | |||
== Misc == | |||
* mxdys made [https://github.com/ccz181078/busycoq/blob/BB6/verify/Inductive_inf.v his inductive decider] for [[History linear|history-linear]] machines compilable into an executable file.<sup>[https://discord.com/channels/960643023006490684/960655108578881597/1501260508051800318]</sup> | |||
== Holdouts == | == Holdouts == | ||
*[[BB(4,3)]] | |||
**Andrew Ducharme reduced the number of holdouts from 5,641,006 to '''5,127,263''', a '''9.11%''' reduction, with mxdys's new inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502750172407533628]</sup> | |||
*[[BB(2,6)]] | *[[BB(2,6)]] | ||
**Andrew Ducharme reduced the number of holdouts from 536,112 to ''' | **Andrew Ducharme reduced the number of holdouts from 536,112 to '''527,232''' via Enumerate.py and TM-enum, a '''1.66%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1500218448951775383][https://discord.com/channels/960643023006490684/1084047886494470185/1501436678823477368]</sup> | ||
**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction. | |||
*[[BB(2,7)]] | *[[BB(2,7)]] | ||
** Terry Ligocki enumerated | ** Terry Ligocki enumerated 30K more subtasks, increasing the number of holdouts to '''775,799,715'''. A total of 250K subtasks out of the 1 million subtasks (or '''25%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659]</sup> | ||
[[Category:This Month in Beaver Research|2026-05]] | [[Category:This Month in Beaver Research|2026-05]] | ||
Latest revision as of 08:44, 10 May 2026
| Prev: April 2026 | This Month in Beaver Research | Next: June 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).
BB Adjacent
- Some new cryptids were hand-built:
- Size 56, by Shawn on 2 May (simulating 5x+1 problem starting at 7).[1]
- Size 49, by aparker, star and Shawn on 3 May (simulating Brocard's problem).[2]
- The first non-trivial divergent GRF was found (size 15). It halts iff there exists some n ≥ 1 such that n+3 divides .[3] aparker[4] and star[5] proved that there is no such n.
Misc
- mxdys made his inductive decider for history-linear machines compilable into an executable file.[6]
Holdouts
- BB(4,3)
- Andrew Ducharme reduced the number of holdouts from 5,641,006 to 5,127,263, a 9.11% reduction, with mxdys's new inductive decider.[7]
- BB(2,6)
- Andrew Ducharme reduced the number of holdouts from 536,112 to 527,232 via Enumerate.py and TM-enum, a 1.66% reduction.[8][9]
- Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to 501,914[10][11], then to 439,120 again using the inductive decider.[12] In total this was a 16.71% reduction.
- BB(2,7)
- Terry Ligocki enumerated 30K more subtasks, increasing the number of holdouts to 775,799,715. A total of 250K subtasks out of the 1 million subtasks (or 25%) have been enumerated.[13]