TMBR: February 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) →Holdouts: Added BB(2,5) progress |
Qwertyasdf (talk | contribs) add info |
||
| (3 intermediate revisions by 2 users not shown) | |||
| Line 4: | Line 4: | ||
[[: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. | ||
== Champions == | |||
* New champions were discovered for [[Busy Beaver for lambda calculus#Champions|BBλ(47)]] and BBλ(95). A [https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/laver.lam BBλ(213) champion] surpassing [https://en.wikipedia.org/wiki/Laver_table q(5)] was discovered by John Tromp and Bertram Felgenhauer. | |||
== Misc == | == Misc == | ||
TODO: independence from Peano (Legion) (see [[Logical independence]]) | TODO: independence from Peano (Legion) (see [[Logical independence]]) | ||
TODO: prurq new fast simulation method (see [https://discord.com/channels/960643023006490684/1471178503235043493 Discord thread]) | |||
== Talks == | == Talks == | ||
| Line 12: | Line 17: | ||
== Holdouts == | == Holdouts == | ||
*[[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]. | |||
**mxdys [https://discord.com/channels/960643023006490684/1259770421046411285/1471229409829847111 announced another TM proven the same day], which turns out to be a translated cycler. | |||
*[[BB(6)]]: 10 machines simulated to 1e13, 3 solved machines. TODO: Update | |||
**prurq [https://discord.com/channels/960643023006490684/1471178503235043493/1471486886890704967 simulated '''10''' machines to 1e13,] lowering the number of machines to simulate out that far to 195. | |||
***Alistaire later simulated another 12 machines to 1e13. | |||
**prurq [https://discord.com/channels/960643023006490684/1239205785913790465/1471831607793946699 found a halting machine] with step count 30505241149212. | |||
**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1471837208615981179 followed up with 2 more halting machines the same day]. All 3 were verified in c++. | |||
** | |||
*[[BB(7)]]: | *[[BB(7)]]: | ||
**Andrew Ducharme has reduced the number of holdouts from 19,303,801 to '''18, | **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. | ||
*[[BB(2,6)]]: | *[[BB(2,6)]]: | ||
**Andrew Ducharme continued reducing the number of holdouts, from 558,039 to 556,814 (a 0.22% reduction) using the newly released mxdys FAR decider. | **Andrew Ducharme continued reducing the number of holdouts, from 558,039 to 556,814 (a 0.22% reduction) using the newly released mxdys FAR decider. | ||
Latest revision as of 16:58, 14 February 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.
Champions
- New champions were discovered for BBλ(47) and BBλ(95). A BBλ(213) champion surpassing q(5) was discovered by John Tromp and Bertram Felgenhauer.
Misc
TODO: independence from Peano (Legion) (see Logical independence)
TODO: prurq new fast simulation method (see Discord thread)
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
- BB(2,5): 2 solved machines.
- Andrew Ducharme found a machine nonhalting on 11 Feb via the newly released mxdys FAR decider. This was verified in Rocq by mxdys the same day.
- mxdys announced another TM proven the same day, which turns out to be a translated cycler.
- BB(6): 10 machines simulated to 1e13, 3 solved machines. TODO: Update
- prurq simulated 10 machines to 1e13, lowering the number of machines to simulate out that far to 195.
- Alistaire later simulated another 12 machines to 1e13.
- prurq found a halting machine with step count 30505241149212.
- mxdys followed up with 2 more halting machines the same day. All 3 were verified in c++.
- prurq simulated 10 machines to 1e13, lowering the number of machines to simulate out that far to 195.
- 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.
- BB(2,6):
- Andrew Ducharme continued reducing the number of holdouts, from 558,039 to 556,814 (a 0.22% reduction) using the newly released mxdys FAR decider.