TMBR: November 2025: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
update vonhust sim description
Talks: Add Tristan's talk
Line 4: Line 4:


== Talks ==
== Talks ==
* Carl Kadie gave a talk on BB during the PyData Seattle 2025 conference: [https://www.youtube.com/watch?v=wSiF1Bm8f3s ''How to make Python programs run very slow (and new Turing Machine results)''] .
* Tristan Stérin gave a talk about [[bbchallenge]] and the [[BB(5)]] proof at Collège de France: [https://www.youtube.com/watch?v=YYrSdaB-6cE Le cinquième nombre Busy Beaver] (in French).[https://discord.com/channels/960643023006490684/1242208042460647575/1435724346051006516]
* (From June) Terence Tao mentioned [[bbchallenge]] in their talk "The Equational Theories Project: advancing collaborative mathematical research at scale" ([https://www.youtube.com/watch?v=T4DE27uk0jw video] / [https://terrytao.wordpress.com/wp-content/uploads/2025/06/math-experiments.pdf slides]) at the [https://www.newton.ac.uk/event/bprw03/ 2025 Big Proof workshop]. The talk is from June, but was just shared on the bbchallenge Discord this month. The talk is about the [https://teorth.github.io/equational_theories/ Equational Theories Project], a large-scale mathematical collaboration that crowd-sourced a proof in Lean. Tao mentions bbchallenge as the only other example of a large-scale mathematical collaboration to prove a single result that he knows of.  
* Carl Kadie gave a talk on BB during the PyData Seattle 2025 conference: [https://www.youtube.com/watch?v=wSiF1Bm8f3s ''How to make Python programs run very slow (and new Turing Machine results)''].[https://discord.com/channels/960643023006490684/960643023530762343/1440090541936214017]
* (From June) Terence Tao mentioned bbchallenge in their talk "The Equational Theories Project: advancing collaborative mathematical research at scale" ([https://www.youtube.com/watch?v=T4DE27uk0jw video] / [https://terrytao.wordpress.com/wp-content/uploads/2025/06/math-experiments.pdf slides]) at the [https://www.newton.ac.uk/event/bprw03/ 2025 Big Proof workshop]. The talk is from June, but was just shared on the bbchallenge Discord this month.[https://discord.com/channels/960643023006490684/960643023530762341/1438442389097287711] The talk is about the [https://teorth.github.io/equational_theories/ Equational Theories Project], a large-scale mathematical collaboration that crowd-sourced a proof in Lean. Tao mentions bbchallenge as the only other example of a large-scale mathematical collaboration to prove a single result that he knows of.  


== Themed Months ==
== Themed Months ==

Revision as of 17:02, 3 December 2025

Prev: October 2025 This Month in Beaver Research Next: December 2025

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).

Talks

Themed Months

There have been two specific BB domain themed months: BB(3,3) month (October) and BB(2,5) month (November). For BB(3,3), this resulted in the clarification of some of the results and techniques on the Discord and Wiki. LegionMammal wrote up a detailed explanation of the probvious halter. No further progress on holdouts was made in October due to the limited number of holdouts and the work that's already been put into trying to solve them. For BB(2,5), it was verified that the Wiki was up to date. @mxdys shared some of his old notes on the unanalyzed machines.

Optimization

  • Discord user vonhust created a fast TM simulator that averages 2 billion steps / s. It uses fixed-block Macro Machines with each block bit-packed into integers, with more optimizations planned. TODO: Sources, details, graph.

BB Adjacent

  • All Fractran deciders
    All Fractran deciders summarized and their relations, shared by Daniel Yuan on 14 Nov 2025
    Busy Beaver for Fractan, or BBf was introduced on 1 Nov by Jason Yuen, who also solved the first 14 values. Then, all values up to 19 were solved, with 19 requiring 3 programs to be proven by hand. For n = 20, 34 holdouts remain, while for n = 21, 587 holdouts are remaining. Three BB-Cryptids were also transformed into Fractran programs, so we know that n = 29 requires solving Hydra.
  • Cyclic Tag was introduced by Discord user Jack on 14 Nov. The first two values, n = 1 and 2 were also solved by him. Then, lower bounds were given for values up to n = 7. CTBB(7) reaches hexation.
  • TODO. Add BMS milestone improved by tromp from 350 to 331. (source: https://discord.com/channels/960643023006490684/1355653587824283678/1436844104742076507)
  • TODO. Add Busy Beaver for SKI calculus.

Holdouts

  • BB(6): Total holdout reduction: 204 TMs, a 12% reduction!
  • BB(2,7): Enumeration started!
    • The code provided by mxdys breaks up the BB(2,7) enumeration into 1 million subtasks which each run for ~10 minutes and leave ~2500 holdouts based on an average of the first 1K subtasks. These values are about 5 times longer than and 25 times larger than the ones for BB(7).
    • Terry Ligocki enumerated the first 3 subtasks, resulting in 88,730,540 holdouts, which can be found here.
    • The expected number of holdouts after the enumeration is ~3B TMs.