TMBR: August 2025: Difference between revisions

Latest revision as of 03:15, 5 September 2025

Prev: July 2025	This Month in Beaver Research	Next: September 2025

This Month in Beaver Research for August 2025. This month, Tristan Stérin presented a poster (see right) at DNA 31, Ben Brubaker wrote a follow-up BB article in Quanta, there were significant holdouts reduction in numerous domains, a fast algorithm for Antihydra (and similar Collatz-like problems) was re-discovered, and multisymbol support was added to the Blaze TM visualizer.

The official bbchallenge BB(5) paper "Determination of the fifth Busy Beaver value" has reached v0.99 and v1.0 will be posted to Arxiv in the first week or two of September.

An early announcement: October will be BB(3,3) month. This is a first test of the idea of "themed focus months". The idea is to encourage broad research focus into the BB(3,3) domain to reduce or describe holdouts more deeply, spread understanding of some of the most complex TMs and analysis techniques, etc. More information will come in next month's TMBR.

In the News

22 Aug 2025. Ben Brubaker. Quanta Magazine. Busy Beaver Hunters Reach Numbers That Overwhelm Ordinary Math.

Cryptids

A fast algorithm for Consistent Collatz simulation was re-discovered and popularized. Using it:

apgoucher simulated Antihydra to $2^{38}$ iterations. This is actually a result from one year ago, but was rediscovered and added to the wiki. https://discord.com/channels/960643023006490684/1026577255754903572/1271528180246773883
Shawn Ligocki simulated 1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC (bbch) out to one additional Collatz reset, demonstrating that (if they halt, which they probviously should) they will have sigma scores $>10^{10^{10^{7}}}$ .

This algorithm has near linear runtime (in the number of iterations simulated), but also linear memory growth since the parameters grow exponentially. This memory limit seems to be the main bottleneck to simulating Antihydra and other Consistent Collatz iterations further. There has been some discussion on more efficient memory usage or a distributed algorithm to support further scaling, but no results are available yet.

Andrew Wade claims to have proven that BB(432) is independent of ZF. https://codeberg.org/ajwade/turing_machine_explorer

Holdouts

In August there were significant reductions in Holdouts lists across many BB Domains

BB Holdout Reduction by Domain
Domain	New Holdout Count	July Holdout Count	Holdout Reduction	% Reduction
BB(6)	2,592	2,728	136	5.0%
BB(2,6)	18,054,938	22,302,296	4,247,358	19.0%
BB(7)	59,727,905	86,129,304	26,401,399	30.7%

BB(6) holdouts: Reduced by a total of 136 holdouts by 4 people.
- XnoobSpeakable found 9 new halting TMs in the high exponential runtime range (~ $10^{100000}$ ) by running Enumerate.py out to extremely high parameters. https://discord.com/channels/960643023006490684/1239205785913790465/1401470301467836556
- Andrew Ducharme found a surprisingly short running halting TM in the BB(6) holdouts list with runtime ~ $10^{78}$ , to which Peacemaker replied with another TM that was almost identical, and soon, simulation showed it to halt in the same number of steps. Later on the 28th, Ducharme found another one with surprisingly low runtime: ~ $10^{11}$ . In response, Peacemaker found an almost identical machine, which also halts with similar runtime.
- Peacemaker shared a list of BB(6) holdouts and how many steps are required to use all defined transitions. https://discord.com/channels/960643023006490684/1239205785913790465/1410437756777398344
- @mxdys shared a list of 7 holdouts that he solved using his RWLAcc decider in Rocq (previously known as Coq). https://discord.com/channels/960643023006490684/1239205785913790465/1408304281039409212 He also shared results featuring 6 holdouts that were solved in "50 Random Holdouts", see https://discord.com/channels/960643023006490684/1400456788955893840/1409115537631613020
- On August 30, @mxdys shared the new holdouts list, consisting of 2,592 TMs. (The additional 110 TMs not listed here were solved by @mxdys using deciders or individual proofs.)
After the enumeration of BB(7) was completed, Andrew Ducharme ran several deciders on the holdouts list, filtering the original 86,129,304 holdouts down to 59,727,905 in 10 days. https://drive.google.com/drive/u/0/folders/17U0BRpJHTMLtB0poBlOSZhGGp4FkCHIO
BB(3,3): 9 holdouts were proven non-halting in Rocq (previously known as Coq) by mxdys. 10 holdouts remain, 4 of them solved with moderate rigor. https://discord.com/channels/960643023006490684/1259770474897080380/1410308974275985428
@mxdys proved 2 BB(2,5) machines are non-halting in Rocq.
Andrew Ducharme reduced the BB(2,6) holdouts from 22,302,296 to 18,054,938. https://discord.com/channels/960643023006490684/1084047886494470185/1412345770241163294

BB Adjacent

John Tromp introduced the $BB\lambda _{1}(n)$ function for Busy Beaver for lambda calculus with an oracle and computed it up to $BB\lambda _{1}(22)$ .
Instruction-Limited Greedy Busy Beaver gBBi(n) and an Instruction-Limited variant of the Blanking Busy Beaver (BLBi(n)) were introduced. gBBi(n) was computed up to n = 13 and BLBi(n) was computed up to n = 7.

Misc

Iijil shared an algorithm for converting an arbitrary n-state m-symbol TM into a 2-state TM with 3(n+1)m symbols. https://gist.github.com/Iijil1/0d611dbf0a9d52984f72cb14e66a4b28
Carl K updated his TM web-visualizer to support multi-symbol machines. https://carlkcarlk.github.io/busy_beaver_blaze/v0.2.6/index.html He also extended his series of videos showing TM simulation accompanied by classical music out to some multi-symbol TMs:
- Bigfoot: https://youtu.be/YvOHWbQNMoY
- Brady's Surprise in a Box: https://youtu.be/vIG2CvJShRc
- BB(2,5) champ: https://youtu.be/QpYBzYDdLEY
- Some interesting BB(2,5) machines: https://youtu.be/CSEKxTpXrDE
@mxdys Introduced "50 Random Holdouts", a thread on the Discord server, where 50 random TMs are selected from the BB(6) holdout list, and everybody focuses on these 50 machines. This month, 6/50 TMs were solved by @mxdys single-handedly.
The community (especially, Andrew Ducharme) proposed a concept "BB(n,m) month", where the community mainly focuses on a single domain, i.e. BB(3,3). The motive of this focused month is to make genuine progress in the one selected domain, with the ultimate goal to reduce all holdouts to Cryptids, with all remaining TMs having been proven in Rocq.

Blog Posts

1 Sep 2025. Katelyn Doucette. All About Space Needle.

Interesting TMs

A collection of interesting TMs that were mentioned on Discord, mostly because of their space-time diagrams or general behavior.

1RB0LE_1RC0RF_1RD---_0LA1RB_1RB1LE_1LD1RF (bbch): Wavy Machine
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE (bbch): Probviously halting Cryptid
1RB1LE_1LC0RA_0RF0LD_1LE1LA_1RC0LB_---1RC (bbch): Unsolved BB(6) TM with pseudorandom behaviour

@@ Line 1: / Line 1: @@
-[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for August 2025, featuring plenty of holdouts reduction in numerous domains, alongside an upgraded TM-visualizer and a couple new BB adjacent games.
+{{TMBRnav|July 2025|September 2025}}
+[[File:Conference poster for DNA31 by Tristan Stérin.png|thumb|396x396px|Conference poster for the [https://dna31.sciencesconf.org/ 31st International Conference on DNA Computing and Molecular Programming], [https://discord.com/channels/960643023006490684/960643023530762341/1409904231468761159 made by Tristan Stérin (cosmo)]]]
+[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for August 2025. This month, [[User:Cosmo|Tristan Stérin]] presented a poster (see right) at DNA 31, Ben Brubaker wrote a follow-up BB article in Quanta, there were significant holdouts reduction in numerous domains, a fast algorithm for [[Antihydra]] (and similar Collatz-like problems) was re-discovered, and multisymbol support was added to the Blaze TM visualizer.
+The official [[bbchallenge]] [[BB(5)]] paper "Determination of the fifth Busy Beaver value" has reached [https://github.com/bbchallenge/bbchallenge-paper/blob/build-paper-pdf/bbchallenge-paper.pdf v0.99] and v1.0 will be posted to Arxiv in the first week or two of September.
+An early announcement: October will be [[BB(3,3)]] month. This is a first test of the idea of "themed focus months". The idea is to encourage broad research focus into the BB(3,3) domain to reduce or describe holdouts more deeply, spread understanding of some of the most complex TMs and analysis techniques, etc. More information will come in next month's TMBR.
+== In the News ==
+* 22 Aug 2025. Ben Brubaker. Quanta Magazine. [https://www.quantamagazine.org/busy-beaver-hunters-reach-numbers-that-overwhelm-ordinary-math-20250822/ Busy Beaver Hunters Reach Numbers That Overwhelm Ordinary Math].
 == Cryptids ==
+A fast algorithm for [[Consistent Collatz]] simulation was re-discovered and popularized. Using it:
+* apgoucher simulated [[Antihydra]] to <math>2^{38}</math> iterations. This is actually a result from one year ago, but was rediscovered and added to the wiki. https://discord.com/channels/960643023006490684/1026577255754903572/1271528180246773883
+* [[User:Sligocki|Shawn Ligocki]] simulated {{TM|1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC}} out to one additional Collatz reset, demonstrating that (if they halt, which they probviously should) they will have sigma scores <math>> 10^{10^{10^7}}</math>.
+This algorithm has near linear runtime (in the number of iterations simulated), but also linear memory growth since the parameters grow exponentially. This memory limit seems to be the main bottleneck to simulating Antihydra and other Consistent Collatz iterations further. There has been some discussion on more efficient memory usage or a distributed algorithm to support further scaling, but no results are available yet.
-* A fast algorithm for [[Consistent Collatz]] simulation was re-discovered and popularized. Using it:
+Andrew Wade claims to have proven that BB(432) is [[Independence from ZFC|independent of ZF]]. https://codeberg.org/ajwade/turing_machine_explorer
-** apgroucher simulated [[Antihydra]] to <math>2^{38}</math> iterations. This is actually a result from one year ago, but was rediscovered and added to the wiki. https://discord.com/channels/960643023006490684/1026577255754903572/1271528180246773883
-** Shawn Ligocki simulated {{TM|1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC}} out to one additional Collatz reset, demonstrating that (if they halt, which they probviously should) they will have sigma scores <math>> 10^{10^{10^7}}</math>.
 == Holdouts ==
+In August there were significant reductions in [[Holdouts lists]] across many [[BB Domains]]
+{| class="wikitable"
+|+BB Holdout Reduction by Domain
+!Domain
+!New Holdout Count
+!July Holdout Count
+!Holdout Reduction
+!% Reduction
+|-
+|[[BB(6)]]
+|2,592
+|2,728
+|136
+|5.0%
+|-
+|[[BB(2,6)]]
+|18,054,938
+|22,302,296
+|4,247,358
+|19.0%
+|-
+|[[BB(7)]]
+|59,727,905
+|86,129,304
+|26,401,399
+|30.7%
+|}
 * [[BB(6)]] holdouts: Reduced by a total of 136 holdouts by 4 people.
-** XnoobSpeakable found 9 new halting TMs in the high exponential runtime range (~<math>10^{100000}</math>) by running Enumerate.py out to extremely high parameters. https://discord.com/channels/960643023006490684/1239205785913790465/1401470301467836556
+** [[User:XnoobSpeakable|XnoobSpeakable]] found 9 new halting TMs in the high exponential runtime range (~<math>10^{100000}</math>) by running Enumerate.py out to extremely high parameters. https://discord.com/channels/960643023006490684/1239205785913790465/1401470301467836556
 ** [https://discord.com/channels/960643023006490684/1239205785913790465/1407580922831831152 Andrew Ducharme found a surprisingly short running halting TM] in the [[BB(6)]] holdouts list with runtime ~<math>10^{78}</math>, to which [https://discord.com/channels/960643023006490684/1239205785913790465/1407659104910053387 Peacemaker replied with another TM] that was almost identical, and soon, simulation showed it to halt in the same number of steps. Later on the 28th, [https://discord.com/channels/960643023006490684/1239205785913790465/1410465964528504872 Ducharme found another one] with surprisingly low runtime: ~<math>10^{11}</math>. In response, [https://discord.com/channels/960643023006490684/1239205785913790465/1410475867200815114 Peacemaker found an almost identical machine], which also halts with similar runtime.
 ** Peacemaker shared a list of BB(6) holdouts and how many steps are required to use all defined transitions. https://discord.com/channels/960643023006490684/1239205785913790465/1410437756777398344
 ** @mxdys shared a list of 7 holdouts that he solved using [https://github.com/ccz181078/busycoq/blob/b1e53d74e5053c3379645aaf75fa8c7a72d00547/verify/RWLAcc.v his RWLAcc decider in Rocq] (previously known as Coq). https://discord.com/channels/960643023006490684/1239205785913790465/1408304281039409212 He also shared results featuring 6 holdouts that were solved in "50 Random Holdouts", see https://discord.com/channels/960643023006490684/1400456788955893840/1409115537631613020
-** On August 30, @mxdys shared the [https://wiki.bbchallenge.org/wiki/Holdouts_lists#Downloadable_Holdout_Lists new holdouts list], consisting of 2,592 TMs. (The additional 110 TMs not listed here were solved by @mxdys using deciders.)
+** On August 30, @mxdys shared the [https://wiki.bbchallenge.org/wiki/Holdouts_lists#Downloadable_Holdout_Lists new holdouts list], consisting of 2,592 TMs. (The additional 110 TMs not listed here were solved by @mxdys using deciders or individual proofs.)
-*After the [[BB(7)#Phase 1|enumeration of BB(7)]] was completed, Andrew Ducharme ran [[BB(7)#Phase 2|several deciders]] on the holdouts list, filtering the original 86,129,304 holdouts down to 59,727,905 in 10 days.https://drive.google.com/drive/u/0/folders/17U0BRpJHTMLtB0poBlOSZhGGp4FkCHIO
+*After the [[BB(7)#Phase 1|enumeration of BB(7)]] was completed, Andrew Ducharme ran [[BB(7)#Phase 2|several deciders]] on the holdouts list, filtering the original 86,129,304 holdouts down to 59,727,905 in 10 days. https://drive.google.com/drive/u/0/folders/17U0BRpJHTMLtB0poBlOSZhGGp4FkCHIO
 *[[BB(3,3)|BB(3,3):]] 9 holdouts were proven non-halting in Rocq (previously known as Coq) by mxdys. [https://wiki.bbchallenge.org/wiki/BB(3,3)#Holdouts 10 holdouts remain, 4 of them solved with moderate rigor.] https://discord.com/channels/960643023006490684/1259770474897080380/1410308974275985428
-*[https://discord.com/channels/960643023006490684/1259770421046411285/1411488532500971631 @mxdys proved] 2 [[BB(2,5)]] machines in Rocq.
+*[https://discord.com/channels/960643023006490684/1259770421046411285/1411488532500971631 @mxdys proved] 2 [[BB(2,5)]] machines are non-halting in Rocq.
+*Andrew Ducharme reduced the [[BB(2,6)]] holdouts from 22,302,296 to 18,054,938. https://discord.com/channels/960643023006490684/1084047886494470185/1412345770241163294
 ==BB Adjacent==
 *John Tromp introduced the <math>BB \lambda _1(n)</math> function for [[Busy Beaver for lambda calculus#Oracle Busy Beaver|Busy Beaver for lambda calculus with an oracle]] and computed it up to <math>BB \lambda _1(22)</math>.
 * Instruction-Limited Greedy Busy Beaver gBBi(n) and an [[Instruction-Limited Busy Beaver#Instruction-Limited Busy Beaver Variants|Instruction-Limited variant]] of the [[Blanking Busy Beaver]] (BLBi(n)) were introduced. gBBi(n) was computed up to n = 13 and BLBi(n) was computed up to n = 7.
-[[Category:This Month in Beaver Research]]
-[[File:Conference poster for DNA31 by Tristan Stérin.png|thumb|396x396px|Conference poster for the [https://dna31.sciencesconf.org/ 31st International Conference on DNA Computing and Molecular Programming], [https://discord.com/channels/960643023006490684/960643023530762341/1409904231468761159 made by Tristan Stérin (cosmo)]]]
 == Misc ==
 * Iijil shared an algorithm for converting an arbitrary n-state m-symbol TM into a 2-state TM with 3(n+1)m symbols. https://gist.github.com/Iijil1/0d611dbf0a9d52984f72cb14e66a4b28
 * Carl K updated his TM web-visualizer to support multi-symbol machines. [https://carlkcarlk.github.io/busy_beaver_blaze/v0.2.6/index.html#palette=edit&colors=000000%2Cff0000%2Cffff00%2Cff00ff%2C00ffff&run=true https://carlkcarlk.github.io/busy_beaver_blaze/v0.2.6/index.html] He also extended his series of videos showing TM simulation accompanied by classical music out to some multi-symbol TMs:
@@ Line 36: / Line 72: @@
 *The community (especially, Andrew Ducharme) [https://discord.com/channels/960643023006490684/992572017683472514/1408559249067479145 proposed a concept "BB(n,m) month",] where the community mainly focuses on a single domain, i.e. BB(3,3). The motive of this focused month is to make genuine progress in the one selected domain, with the ultimate goal to reduce all holdouts to [[Cryptids]], with all remaining TMs having been proven in Rocq.
-==In the News==
+==Blog Posts==
+* 1 Sep 2025. Katelyn Doucette. [https://katelyndoucette.com/articles/all-about-space-needle All About Space Needle].
-* 22 Aug 2025. Ben Brubaker. Quanta Magazine. [https://www.quantamagazine.org/busy-beaver-hunters-reach-numbers-that-overwhelm-ordinary-math-20250822/ Busy Beaver Hunters Reach Numbers That Overwhelm Ordinary Math].
 ==Interesting TMs==
@@ Line 44: / Line 79: @@
 * {{TM|1RB0LE_1RC0RF_1RD---_0LA1RB_1RB1LE_1LD1RF}}: Wavy Machine
-* {{TM|1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE}}: Probviously halting cryptid
+* {{TM|1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE}}: [[Probviously]] halting Cryptid
 * <code>[[1RB1LE_1LC0RA_0RF0LD_1LE1LA_1RC0LB_---1RC]]</code> ([https://bbchallenge.org/1RB1LE_1LC0RA_0RF0LD_1LE1LA_1RC0LB_---1RC bbch]): Unsolved BB(6) TM with pseudorandom behaviour
-[[Category:This Month in Beaver Research]]
+[[Category:This Month in Beaver Research|2025-08]]