TMBR: February 2026: Difference between revisions
RobinCodes (talk | contribs) Finalizing TMBR |
RobinCodes (talk | contribs) →Misc: List format for Misc section |
||
| Line 9: | Line 9: | ||
== Misc == | == Misc == | ||
Discord user prurq announced a new simulation method, "Cascade", which works especially well, see [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 Discord thread]. | * @LegionMammal978 created two new nonhalting machines, whose halting status is independent of the theories of [https://en.wikipedia.org/w/index.php?title=Peano_Arithmetic Peano Arithmetic] (BB(372)) and ZFC+"There exist arbitrarily large [[wikipedia:Subtle_cardinal|subtle cardinals]]" (BB(493)) (see [[Logical independence]]) | ||
* Discord user prurq announced a new simulation method, "Cascade", which works especially well, see [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 Discord thread]. | |||
@mxdys [https://discord.com/channels/960643023006490684/1226543091264126976/1469937272752177298 introduced a new longitudinal acceleration method], which [https://discord.com/channels/960643023006490684/1239205785913790465/1473950417275850804 had very fruitful results]. | * @mxdys [https://discord.com/channels/960643023006490684/1226543091264126976/1469937272752177298 introduced a new longitudinal acceleration method], which [https://discord.com/channels/960643023006490684/1239205785913790465/1473950417275850804 had very fruitful results]. | ||
== Talks == | == Talks == | ||
Latest revision as of 13:36, 7 March 2026
| Prev: January 2026 | This Month in Beaver Research | Next: March 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 February 2026. This month, we had an amazing reduction in BB(6) holdouts, as well as a nice reduction in the BB(7) holdouts. We again had the chance to see a rare occurence: two BB(2,5) machines were proven nonhalting this month. A new simulation method was introduced by prurq - see Discord. Legion created two new nonhalting machines, whose halting status is independent of the theories of Peano Arithmetic (372-state) and ZFC + "There exist arbitrarily large subtle cardinals" (493-state) - See Logical independence. Moreover, Tristan Stérin announced that the paper "Determination of the fifth Busy Beaver value" was accepted for the 58th ACM Symposium on Theory of Computing (STOC 2026), and there would be a talk at the event in Salt Lake City in June 2026.
Champions
- New champions were discovered for BBλ(47) and BBλ(95). A BBλ(201) champion surpassing q(5) was discovered by John Tromp, Bertram Felgenhauer, and 50_ft_lock.
Misc
- @LegionMammal978 created two new nonhalting machines, whose halting status is independent of the theories of Peano Arithmetic (BB(372)) and ZFC+"There exist arbitrarily large subtle cardinals" (BB(493)) (see Logical independence)
- Discord user prurq announced a new simulation method, "Cascade", which works especially well, see Discord thread.
- @mxdys introduced a new longitudinal acceleration method, which had very fruitful results.
Talks
- Tristan Stérin announced that the paper "Determination of the fifth Busy Beaver value" was accepted for the 58th ACM Symposium on Theory of Computing (STOC 2026), and there would be a talk at the event in Salt Lake City in June 2026
Holdouts
| Domain | Previous Holdout Count | New Holdout Count | Holdout Reduction | % Reduction |
|---|---|---|---|---|
| BB(2,5) | 74 | 72 | 2 | 2.70% |
| BB(6) | 1314 | 1214 | 100 | 7.61% |
| BB(7) | 19,303,801 | 18,195,192 | 1,108,609 | 5.74% |
| BB(2,6) | 558,039 | 548,993 | 9,046 | 1.62% |
- BB(2,5): 2 solved machines.
- Andrew Ducharme found a machine nonhalting on 11 Feb via the mxdys C++ FAR decider. This was verified in Rocq by mxdys the same day.
- mxdys announced another TM proven the same day, which turned out to be a translated cycler.
- Peacemaker II found the high-level behaviour of a machine, which turned out to be a relatively simple-to-describe string rewriting problem of sorts.
- BB(6): All machines simulated to 1e13, 100 solved machines.
- prurq found a halting machine with step count 30,505,241,149,212.
- mxdys followed up with 2 more halting machines the same day. All 3 were verified in c++.
- Andrew Ducharme found 7 non-halting machines using the mxdys C++ FAR decider.
- Alistaire found a machine nonhalting using Quick_Sim.py.
- prurq simulated 38 machines for >1e13 steps[19 machines][19 more machines] with his new method "Cascade".
- Alistaire simulated 13 machines for >1e13 steps, 6 of which had already been simulated by prurq, essentialy double-verifying them.
- Discord user @mammillaria simulated a TM for >1e13 steps, which also turned out to have been simulated by prurq already.
- For all machines simulated by prurq, see: Spreadsheet, for all simulated by Alistaire (most machines), see: [1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17]. All machines but 3: [18] were ran to 1e13.
- Though on March 1st, most of the work was probably done in February: prurq simulated the remaining machines to 1e13.[19]
- mxdys released a holdouts list of 1226 machines up to equivalence, some of which were decided via new mxdys method for longitudinal acceleration.
- Andrew Ducharme found 9 non-halting machines in that list using the mxdys C++ FAR decider.[20][21][22]
- mxdys released another holdouts list of 1214 machines up to equivalence.
- At the end of the month, the formal and Rocq-verified holdout counts are 1214, the informal holdout count is 1212.
- BB(7):
- Andrew Ducharme has reduced the number of holdouts from 19,303,801 to 18,254,545 (a 5.44% reduction) and then 18,195,192 (0.33%) using the mxdys C++ FAR decider.
- BB(2,6):
- Andrew Ducharme continued reducing the number of holdouts, from 558,039 to 551,586 (a 1.16% reduction) using the mxdys C++ FAR decider.
- Another 0.47% reduction by Andrew Ducharme left 548,993 holdouts.[23]