TMBR: February 2026: Difference between revisions
Jump to navigation
Jump to search
→Holdouts: added new BB(6) holdouts list |
RobinCodes (talk | contribs) More todo |
||
| (9 intermediate revisions by 4 users not shown) | |||
| Line 3: | Line 3: | ||
''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).'' | ||
[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for February 2026. | [[:Category:This Month in Beaver Research|This Month in Beaver Research]] for February 2026. TODO: Write a proper introductory paragraph. | ||
== Champions == | == Champions == | ||
| Line 9: | Line 9: | ||
== Misc == | == Misc == | ||
@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]]) | |||
TODO: prurq new fast simulation method (see [https://discord.com/channels/960643023006490684/1471178503235043493 Discord thread]) | TODO: prurq new fast simulation method (see [https://discord.com/channels/960643023006490684/1471178503235043493 Discord thread]) | ||
TODO: "Cascade" (see [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 Discord thread] ) | TODO: "Cascade" (see [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 Discord thread] ) | ||
TODO: new longitudinal acceleration method, see [https://discord.com/channels/960643023006490684/1226543091264126976/1469937272752177298 Discord] | |||
== Talks == | == Talks == | ||
| Line 19: | Line 21: | ||
== Holdouts == | == Holdouts == | ||
{| class="wikitable" | |||
|+BB Holdout Reduction by Domain | |||
!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.''' | *[[BB(2,5)]]: '''2 solved machines.''' | ||
**Andrew Ducharme found a machine nonhalting on [https://discord.com/channels/960643023006490684/1259770421046411285/1471227102844944510 11 Feb] via the | **Andrew Ducharme found a machine nonhalting on [https://discord.com/channels/960643023006490684/1259770421046411285/1471227102844944510 11 Feb] via the mxdys C++ FAR decider. This was verified in Rocq by mxdys [https://discord.com/channels/960643023006490684/1259770421046411285/1471228798505582602 the same day]. | ||
**mxdys [https://discord.com/channels/960643023006490684/1259770421046411285/1471229409829847111 announced another TM proven the same day], which turned out to be a translated cycler. | **mxdys [https://discord.com/channels/960643023006490684/1259770421046411285/1471229409829847111 announced another TM proven the same day], which turned out to be a translated cycler. | ||
**Peacemaker II [https://discord.com/channels/960643023006490684/1259770421046411285/1472647706835943596 found the high-level behaviour of a machine], which turned out to be a relatively simple-to-describe string rewriting problem of sorts. | **Peacemaker II [https://discord.com/channels/960643023006490684/1259770421046411285/1472647706835943596 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)]]: ''' | *[[BB(6)]]: '''All''' '''machines simulated to 1e13''', '''100''' solved machines. | ||
**prurq [https://discord.com/channels/960643023006490684/1239205785913790465/1471831607793946699 found a halting machine] with step count 30,505,241,149,212. | ** prurq [https://discord.com/channels/960643023006490684/1239205785913790465/1471831607793946699 found a halting machine] with step count 30,505,241,149,212. | ||
**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1471837208615981179 followed up with 2 more halting machines the same day]. All 3 were verified in c++. | ** mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1471837208615981179 followed up with 2 more halting machines the same day]. All 3 were verified in c++. | ||
**Andrew Ducharme [https://discord.com/channels/960643023006490684/1239205785913790465/1472051232746115173 found 7 non-halting machines] using the | ** Andrew Ducharme [https://discord.com/channels/960643023006490684/1239205785913790465/1472051232746115173 found 7 non-halting machines] using the mxdys C++ FAR decider. | ||
**Alistaire [https://discord.com/channels/960643023006490684/1239205785913790465/1472376779825090713 found a machine nonhalting] using Quick_Sim.py. | ** Alistaire [https://discord.com/channels/960643023006490684/1239205785913790465/1472376779825090713 found a machine nonhalting] using Quick_Sim.py. | ||
**prurq simulated 38 machines for >1e13 steps<sup>[https://discord.com/channels/960643023006490684/1471178503235043493/1471486886890704967 <nowiki>[19 machines]</nowiki>][https://docs.google.com/spreadsheets/d/1zMhtW_edMxrfUry-hVMFsDg3T1p_udjC2V2RKu6oSKE/edit?usp=sharing <nowiki>[19 more machines]</nowiki>]</sup> with his new method [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 "Cascade".] | ** prurq simulated 38 machines for >1e13 steps<sup>[https://discord.com/channels/960643023006490684/1471178503235043493/1471486886890704967 <nowiki>[19 machines]</nowiki>][https://docs.google.com/spreadsheets/d/1zMhtW_edMxrfUry-hVMFsDg3T1p_udjC2V2RKu6oSKE/edit?usp=sharing <nowiki>[19 more machines]</nowiki>]</sup> with his new method [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 "Cascade".] | ||
**Alistaire [https://discord.com/channels/960643023006490684/1239205785913790465/1472246267345113158 simulated 13 machines] for >1e13 steps, 6 of which had already been simulated by prurq, essentialy double-verifying them. | ** Alistaire [https://discord.com/channels/960643023006490684/1239205785913790465/1472246267345113158 simulated 13 machines] for >1e13 steps, 6 of which had already been simulated by prurq, essentialy double-verifying them. | ||
**Discord user @mammillaria [https://discord.com/channels/960643023006490684/1239205785913790465/1472325414344069271 simulated a TM] for >1e13 steps, which also turned out to have been simulated by prurq already. | ** Discord user @mammillaria [https://discord.com/channels/960643023006490684/1239205785913790465/1472325414344069271 simulated a TM] for >1e13 steps, which also turned out to have been simulated by prurq already. | ||
** | ** For all machines simulated by prurq, see: [https://docs.google.com/spreadsheets/d/1zMhtW_edMxrfUry-hVMFsDg3T1p_udjC2V2RKu6oSKE/edit?gid=0#gid=0 Spreadsheet], for all simulated by Alistaire (most machines), see: [https://discord.com/channels/960643023006490684/1239205785913790465/1472246267345113158 <nowiki>[1]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1472376779825090713 <nowiki>[2]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1472749954715095181 <nowiki>[3]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1473010093284130847 <nowiki>[4]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1473035474745692351 <nowiki>[5]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1473442168927686677 <nowiki>[6]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1473785617208053900 <nowiki>[7]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1474120868761174040 <nowiki>[8]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1474178147036434609 <nowiki>[9]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1474508316335144993 <nowiki>[10]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1474685965409976561 <nowiki>[11]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1474903012446306354 <nowiki>[12]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475203181867958375 <nowiki>[13]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475272630478049371 <nowiki>[14]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475564139438014554 <nowiki>[15]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475778581287403551 <nowiki>[16]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475922318915272734 <nowiki>[17]</nowiki>]. '''All machines but 3: [https://discord.com/channels/960643023006490684/1239205785913790465/1474508720330375460 <nowiki>[18]</nowiki>] were ran to 1e13.''' | ||
**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1473950417275850804 released] a [[holdouts list]] of 1226 machines up to equivalence, some of which were decided via [https://discord.com/channels/960643023006490684/1226543091264126976/1469937272752177298 new mxdys method for longitudinal acceleration]. | ** Though on March 1st, most of the work was probably done in February: prurq '''simulated the remaining machines to 1e13'''.[https://discord.com/channels/960643023006490684/1477591686514212894/1477716122617905305 <nowiki>[19]</nowiki>] | ||
**Andrew Ducharme found 9 non-halting machines in that list using the mxdys FAR decider.[https://discord.com/channels/960643023006490684/1239205785913790465/1474302212284092436][https://discord.com/channels/960643023006490684/1239205785913790465/1475911180965904577][https://discord.com/channels/960643023006490684/1239205785913790465/1477040884728987820] | ** mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1473950417275850804 released] a [[holdouts list]] of '''1226''' machines up to equivalence, some of which were decided via [https://discord.com/channels/960643023006490684/1226543091264126976/1469937272752177298 new mxdys method for longitudinal acceleration]. | ||
**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1477224991136419983 released] another holdouts list of 1214 machines up to equivalence. | ** Andrew Ducharme found 9 non-halting machines in that list using the mxdys C++ FAR decider.[https://discord.com/channels/960643023006490684/1239205785913790465/1474302212284092436 <nowiki>[20]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1475911180965904577 <nowiki>[21]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1477040884728987820 <nowiki>[22]</nowiki>] | ||
** mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1477224991136419983 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)]]: | *[[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 | **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)]]: | *[[BB(2,6)]]: | ||
**Andrew Ducharme continued reducing the number of holdouts, from 558,039 to '''551,586''' (a 1.16% reduction) using the mxdys FAR decider. | **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.[https://discord.com/channels/960643023006490684/1084047886494470185/1475216024734269644 <nowiki>[23]</nowiki>] | |||
[[Category:This Month in Beaver Research|2026-02]] | [[Category:This Month in Beaver Research|2026-02]] | ||
Latest revision as of 18:01, 1 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. TODO: Write a proper introductory paragraph.
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)
TODO: prurq new fast simulation method (see Discord thread)
TODO: "Cascade" (see Discord thread )
TODO: new longitudinal acceleration method, see Discord
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]