TMBR: February 2026: Difference between revisions
Jump to navigation
Jump to search
→Holdouts: added table of reductions |
→Holdouts: switched order of the holdout counts in the table |
||
| Line 22: | Line 22: | ||
|+BB Holdout Reduction by Domain | |+BB Holdout Reduction by Domain | ||
!Domain | !Domain | ||
!Previous Holdout Count | |||
!New Holdout Count | !New Holdout Count | ||
!Holdout Reduction | !Holdout Reduction | ||
!% Reduction | !% Reduction | ||
|- | |- | ||
|[[BB(2,5)]] | |[[BB(2,5)]] | ||
|74 | |||
|72 | |72 | ||
|2 | |2 | ||
|2.70% | |2.70% | ||
Revision as of 10:20, 28 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λ(201) champion surpassing q(5) was discovered by John Tromp, Bertram Felgenhauer, and 50_ft_lock.
Misc
TODO: independence from Peano (Legion) (see Logical independence)
TODO: prurq new fast simulation method (see Discord thread)
TODO: "Cascade" (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
| 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 newly released mxdys 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): XX machines simulated to 1e13, XX solved machines. TODO: Update
- 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 newly released mxdys 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.
- 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
- 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 FAR decider.[1][2][3]
- mxdys released another holdouts list of 1214 machines up to equivalence.
- 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 551,586 (a 1.16% reduction) using the mxdys FAR decider.
- Another 0.47% reduction by Andrew Ducharme left 548,993 holdouts.[4]