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 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.
  • 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): 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 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.
  • After all, 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 C++ 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 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.[4]