TMBR: May 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) →Holdouts: Added BB(2,6) progress |
Added mxdys inductive decider |
||
| Line 10: | Line 10: | ||
** 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> | ** 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. | * 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 == | ||
Revision as of 09:58, 9 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]