TMBR: 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

• 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): 45 machines simulated to 1e13, 11 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 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.
  • mxdys released a holdouts list of 1226 machines up to equivalence.
  • Andrew Ducharme found 2 non-halting machines in that list using the newly released mxdys FAR decider.
• 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.