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. This month, we had an excellent reduction in BB(6) holdouts, as well as a nice reduction in the BB(7) holdouts. Amazingly, we saw two BB(2,5) machines were proven nonhalting for the second month in a row. @LegionMammal978 created two new machines whose halting status is independent of the theories of Peano Arithmetic (372-state) and ZFC paired with the axiom "There exist arbitrarily large subtle cardinals" (493-state). For more context, see Logical independence. A new simulation method was introduced by @prurq - see Discord. Moreover, Tristan Stérin announced that the paper "Determination of the fifth Busy Beaver value" was accepted to the prestigious 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.

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)
• Discord user prurq announced a new simulation method, "Cascade", which works especially well, see Discord thread.
• @mxdys introduced a new longitudinal acceleration method, which had very fruitful results.

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): All machines simulated to 1e13, 100 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 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.
  • For all machines simulated by prurq, see: Spreadsheet, for all simulated by Alistaire (most machines), see: [1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17]. All machines but 3: [18] were ran to 1e13.
  • Though on March 1st, most of the work was probably done in February: prurq simulated the remaining machines to 1e13.[19]
  • 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.[20][21][22]
  • mxdys 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):
  • 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.[23]