TMBR: February 2026: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
Polygon (talk | contribs)
Holdouts: switched order of the holdout counts in the table
RobinCodes (talk | contribs)
More todo
 
(7 intermediate revisions by 3 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 ==
TODO: independence from Peano (Legion) (see [[Logical independence]])
@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 52: Line 54:
|}
|}
*[[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 newly released mxdys FAR decider. This was verified in Rocq by mxdys [https://discord.com/channels/960643023006490684/1259770421046411285/1471228798505582602 the same day].
**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)]]: '''XX''' machines simulated to 1e13, '''XX''' solved machines. TODO: Update
*[[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 newly released mxdys FAR decider.
** 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.
**Afterall, the informal holdout count is '''1299''', and the formal holdout count is 1303 (8 newly solved machines were solved by highly trusted code, 4 informal TMs beforehand). Rocq-verified holdout count is 1314. There remain '''160''' machines to be simulated up to 1e13. TODO: Update
** 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 newly released mxdys FAR decider.
**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]
**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

Holdouts

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%