TMBR: February 2026

Prev: January 2026

This Month in Beaver Research

Next: March 2026

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 Turing machines whose halting status is independent of the theories of Peano Arithmetic (372-state)^[1] and ZFC paired with the axiom "There exist arbitrarily large subtle cardinals" (493-state)^[2]. 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 Turing machines, whose halting status is independent of the theories of Peano Arithmetic (BB(372)^[3] and ZFC+"There exist arbitrarily large subtle cardinals" (BB(493))^[4] (see Logical independence for more context and the machines)
• 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

• Shawn Ligocki gave a 6min talk about Busy Beaver at Gathering 4 Gardner 16 in San Francisco on 19 Feb. The talk was recorded, but is not available yet (as of Apr 2026).
• 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 determined the high-level behaviour of a holdout could be transformed into a relatively simple-to-describe string rewriting problem.
• 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, essentially 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^{[3 machines]} were ran to 1e13.
  • Though announced on March 1st, prurq simulated the remaining machines to 1e13.^[5]
  • mxdys released a holdouts list of 1226 machines up to equivalence, some of which were decided via a new mxdys method for longitudinal acceleration.
  • Andrew Ducharme found 9 non-halting machines in that list using the mxdys C++ FAR decider.^[6][7][8]
  • 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 to 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.^[9]