The Busy Beaver Challenge: https://bbchallenge.org

[Tristan Stérin]

Dear all,

I just have been introduced to your group by Pascal Michel, and your work and dedication to the Busy Beaver problem is extremely impressive.

My name is Tristan Stérin and I am a final year PhD student in computer science under supervision of Damien Woods at the University of Maynooth, Ireland.

I recently created the collaborative platform https://bbchallenge.org of which goal is to collaboratively solve the conjecture BB(5) = 47,176,870. With the website, you can share TMs via URL: https://bbchallenge.org/43374927 or https://bbchallenge.org/1RB1LC1RC1RB1RD0LE1LA1LD---0LA&status=halt

To do so, we have used key elements of the method of Marxen & Buntrock, 1990 with a few differences:

1. We have decoupled the enumeration of 5-state Turing machines from the task of applying forward/backward reasoning to it. From this yields:
   1. A publicly available "seed database" of 88,664,064 undecided machines to study
   2. A collection of "deciders" which are small programs dedicated to deciding certain types of machines. The aim is to prove that these programs are correct in order to augment the trust in our results.
      
      
2. We aim at giving a classification, a "zoology", of forward behaviors of 5-state Turing machines. The current zoology is available on the main page and is collaborative.
   
   
3. We aim at having all the contributions to this project to be open-source and proven correct, see our statement on this matter. To help with collaboration, we have a forum and a discord channel.

To date, three deciders have been applied and proven correct which currently leaves 1,330,882 machines undecided. It is not nearly as good as the reported results of Marxen & Buntrock, 1990 or Skelet's but we aim to take the time to prove every step of the way.

We are currently trying to decide so-called "Unilateral bouncers" and "Bilateral bouncers" such as https://bbchallenge.org/9281450 or https://bbchallenge.org/76727755 which we estimate represent around 90% of the remaining undecided machines.

More information is given at:

• https://bbchallenge.org/story
  
• https://bbchallenge.org/method

I would be truly honored to discuss this platform with you and answer any concerns, comments or correct any misinformation that you would find on the website.

Of course, you are all more than welcome to contribute to the project and I would be more than happy to harmonize any vocabulary or convention to make it more appealing to your community.

Sincerely yours,

Tristan Stérin

https://dna.hamilton.ie/tsterin/

[Shawn Ligocki]

Welcome Tristan, it's fantastic to meet you! I absolutely love this website and collaboration idea. When I get a chance, I will be interacting more on the forum to share decider algorithms and discuss approaches.

One of my pie-in-the-sky dreams has been to prove BB results programmatically (in Coq or Lean) so I was very excited to see your note about that being a potential interest to you as well (although I agree that it would be a massive additional effort ... even to prove BB(4, 2) :) ... still if anyone else is seriously interested in looking into this, I am extremely interested in investigating and putting time into this endeavor!).

In case you are interested, my father Terry and I maintain an open-source codebase for BB enumeration, proving, simulation and analysis. It is mostly in Python with a few things optimized in C++ (and I was serendipitously just thinking about a golang version :) ). With it we have been able to reduce the 5x2 BB down to ~6k undecided machines. I'm excited to try and integrate some of our methods (mostly from Marxen).

Another thing I've become interested in recently is some sort of computer readable "proof certificate" that a decider could produce which a smaller (more trusted) piece of code could verify. This would have many potential benefits: 1) simplified verifier to search for bugs / prove correctness of / write in Lean/Coq, etc; 2) Interoperability between deciders in different languages/libraries; 3) ability for people to submit custom (hand-written) proofs for specific machines that could (potentially) still be machine verified (verification is easier than finding a proof). But it would be difficult to figure out how these certificates would work exactly.

What a small world: Please tell Damien I say hello! We met over a decade ago when he was visiting Erik Winfree's lab at Caltech (where I worked for a year) and have corresponded a few times on Busy Beaver topics :)

-Shawn

--
You received this message because you are subscribed to the Google Groups "Busy Beaver Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to busy-beaver-dis...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/000d3655-82e9-4ef3-9975-bf4885ae1401n%40googlegroups.com.

[Tristan Stérin]

Great to meet you too!!

Yes, I absolutely agree with the ambition to write these proofs in Coq or Lean :D

I have an idea that might make it "not too hard": write proof templates and let deciders fill in the parameters for each machine. For instance, take the simplest family of "Cyclers" (machines that just repeat configurations forever). It is a by-product of the algorithm that decide them that we get all the information that we need for a proof of non-termination: (a) the time of the first occurrence of the first repeated configuration and (b) the time of the second occurrence of the second repeated configuration. You then just have to write a Lean/Coq template that deduces non-termination once its given these parameters.

In fact, I believe that as soon as you have a proof of correctness for your decider algorithm (such as these proofs), you can in theory deduce a proof template for all the machines that it decides. We would end up with millions of individual proofs compiled from those deciders' templates and would "just" need the compute power to run them all through Lean/Coq. Although, I have no experience with Lean/Coq so this is all very hypothetical :D This idea of proof templates might be exactly also what you were thinking with proof certificates!

Thank you very much for sharing your codebase!! I am definitely interested in it, I am going to dig into it !! Congrats on the 6k machines, that is extremely impressive!

I will definitely pass on the hello to Damien who was the first one to introduce me to your and your father's BB exploits.

Thank you also for creating this group, I am very happy to have found a place to discuss this fascinating subject.

Sincerely yours,

[Shawn Ligocki]

Yeah, I think that your idea of "proof templates" in Coq/Lean is the strongest example of my proof certificates idea. A looser example would be something more akin to a formalized version of one of my blog posts proving that a TM halts (like this one, say). So it would be some formal way to list rules like this and enough information for a verifier to validate them.

I have some limited experience with Coq (Proving unique prime factorization for integers). Enough to know this would not be an easy task at all, but I also have a lot of ideas about how to approach it and I think it's within reach to a group of 2-3 or so committed folks :)

To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/da90c442-1cc0-4474-818d-39e5478a4f43n%40googlegroups.com.

[Tristan Stérin]

I like your blog post!! Collatz-like maps are fascinating... 

Intuitively Lean seems more "modern" and with a more accessible community than Coq to me, but this feeling is not based on anything concrete. A good starting point might be to write the proof of non termination of a Cycler and then generalise that to its proof template and see how it works.

An interesting thing to me is that proofs of non-termination can get arbitrarily mathematically hard. For instance, with 27 states you get Goldbach's conjecture (there is a 27-state machine that halts iff it has found a counterexample to it), with ~700 states you get the Riemann Hypothesis and even the consistency of ZFC. A great reference on the subject is this paper by Scott Aaronson: https://www.scottaaronson.com/papers/bb.pdf. With Damien, we proved that even with as low as 15 states you get a conjecture by Erdõs open for decades: https://arxiv.org/abs/2107.12475. Hence the complexity of non-termination proofs augments at each state that you add to your machines.

I am interested in getting an idea of the spectrum of proof complexity within 5-state machines. My dream, to be honest, would be that there is a 5-state machine for which no one is able to prove non-termination. That would give, on the BB/TM scale the simplest open problem in mathematics...

Don't hesitate to let me know if you are considering to take concrete steps in the direction of automatic proving, I'd be happy to be part of it,

[Nicholas Drozd]

I too have enough experience with formal proofs to know that this sounds difficult! My suggestion would be to start the 2-state case and work up from there. It seems like it ought to be easy, but I bet it isn't.

For the solvable cases (2, 3, 4 states), the basic structure of the proof looks like the proof of the four color theorem. First you prove that if certain conditions obtain for a given instance, the theorem is true for it. Then you have to prove that those conditions obtain for every instance, and there are only finitely many to check. It's "just" a matter of getting the verifier to believe all that!

Then you have 5 states. IMO it's likely that there are already 5-state programs with halt instructions that don't halt and cannot be proved not to halt. Or at least, proving that they don't halt is equivalent to proving that some Collatz-like function doesn't terminate. That would require some substantial math, to say the least, and might be literally impossible.

I think the most valuable part of the whole endeavor would be to prove formally that some machine implements some Collatz-like function. Even stating that claim to a theorem prover is non-trivial.

[Shawn Ligocki]

Yes, sadly the fragmentation in the formal proof system ecosystem is slightly frustrating. Both Coq and Lean are based on the same basic mathematical system and have extremely similar syntax, but are sadly not compatible :/ I think that Coq is a lot more mature and has been used to prove a lot of amazing things in the academic/industry CS side (certified C compiler, encryption algorithm, etc.). But I agree that from what I can tell Lean has a much more welcoming community especially for bringing in folks from Mathematics. And Lean does have a Turing Machine definition in it's mathlib. This is a critical and non-trivial first step to accomplishing anything there. I'm not 100% sure if we'd be able to reuse it though, the twiddly details could be slightly different than what we want.

Indeed, everything about the Busy Beaver effort rests on this knife's edge between provable and unprovable! My guess is that we may never be able to prove (or maybe even find) even BB(6) (and almost certainly BB(7)). But BB(5) does feel like it is within reach! (Although, I see that Nick thinks even BB(5) may be outside our reach :) ) Your 15-state TM paper looks quite interesting! I love to read about the complex behavior of surprisingly small machines!

I like your flipping of the pessimistic view to the optimistic: That finding a machine which nobody can prove would be a positive, exciting find :) I think I agree and that codifying those machines more clearly and putting out a challenge for folks to try and wrangle it would be exciting as well!

To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/f71a18fb-1cb9-417d-ac69-85d43efd94dbn%40googlegroups.com.

[Terry Ligocki]

I'm a bit behind on this even though it's only been about a day since Tristan's first message. That's a very good thing! I'm in the midst of retiring (two days left) and all the BB/TM activity in the time is wonderful but it's excruciating to be otherwise busy right now, 🥴.

In any case, what Tristan is doing meshes well with everything that has been done to make resources for the BB/TM problems available on the internet and accessible to anyone. Shawn and I benefited greatly in the early 2000's from online resources like Pascal's and Heiner's. Rensselaer also has a BB effort and had compiled a lot of result for the BB(5) case: https://homepages.hass.rpi.edu/heuveb/Research/bb.html and https://homepages.hass.rpi.edu/heuveb/Research/BB/index.html. It looks like most (all) of the links on the latter page are broken BUT it would be worth tiring to see if some of that work could be recovered and added to an active page somewhere (e.g., https://bbchallenge.org).

In general, I would like to be part of an effort to build a BB/TM site that had some type of permanence (like Pascal's and Heiner's) and continued to grow and serve researchers interested in BB/TM problems and exploration. In addition to research results and code, it include all TMs so far enumerated and analyzed (and how they were analyzed). This would provide a resource to explore TMs of various sizes and ask new and different questions without a researcher having to enumerate and analyze the TMs themselves (i.e., build on past explorations and research).

So, I have to end this message to complete my retirement but I'm looking forward to having the time and energy to contribute to this new effort to do research and provide results...

                                Terry J. (Ligocki, tjli...@gmail.com)

--
You received this message because you are subscribed to the Google Groups "Busy Beaver Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to busy-beaver-dis...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/000d3655-82e9-4ef3-9975-bf4885ae1401n%40googlegroups.com.

---

I'm going to throw up!
I'm an engineer, goddamn it!

       - 2010: The Year We Make Contact (John Lithgow)

[Tristan Stérin]

> I think the most valuable part of the whole endeavor would be to prove formally that some machine implements some Collatz-like function. Even stating that claim to a theorem prover is non-trivial.

I completely agree with you that Collatz-hardness must quickly sneak around when looking at these systems.

> Yes, sadly the fragmentation in the formal proof system ecosystem is slightly frustrating. Both Coq and Lean are based on the same basic mathematical system and have extremely similar syntax, but are sadly not compatible :/ I think that Coq is a lot> > more mature and has been used to prove a lot of amazing things in the academic/industry CS side (certified C compiler, encryption algorithm, etc.). But I agree that from what I can tell Lean has a much more welcoming community especially for >bringing in folks from Mathematics. And Lean does have a Turing Machine definition in it's mathlib. This is a critical and non-trivial first step to accomplishing anything there. I'm not 100% sure if we'd be able to reuse it though, the twiddly details could be > slightly different than what we want.

Its very cool if Lean has some groundwork on TMs because hopefully it could be adapted to our use-case.  Maybe we could organise an online workshop in the future with as a goal to try and setup the premises of an automatic proving system for BB(<= 5). I am also interested in looking at what are the deciders that you need for BB(5) that you don't need for BB(4), i.e. trying to have a very precise idea of the new kinds of behaviors that this 1 more state allow.

> I'm a bit behind on this even though it's only been about a day since Tristan's first message. That's a very good thing! I'm in the midst of retiring (two days left) and all the BB/TM activity in the time is wonderful but it's excruciating to be otherwise busy right now, 🥴.

Waw!! Good luck, I can't imagine how tiring it must be.

> In any case, what Tristan is doing meshes well with everything that has been done to make resources for the BB/TM problems available on the internet and accessible to anyone. Shawn and I benefited greatly in the early 2000's from online resources >like Pascal's and Heiner's. Rensselaer also has a BB effort and had compiled a lot of result for the BB(5) case: https://homepages.hass.rpi.edu/heuveb/Research/bb.html and https://homepages.hass.rpi.edu/heuveb/Research/BB/index.html. It looks like >most (all) of the links on the latter page are broken BUT it would be worth tiring to see if some of that work could be recovered and added to an active page somewhere (e.g., https://bbchallenge.org).

Thank you for these links, I had never come across them. I must dig around and reference the results on bbchallenge's page.

> In general, I would like to be part of an effort to build a BB/TM site that had some type of permanence (like Pascal's and Heiner's) and continued to grow and serve researchers interested in BB/TM problems and exploration. In addition to research >results and code, it include all TMs so far enumerated and analyzed (and how they were analyzed). This would provide a resource to explore TMs of various sizes and ask new and different questions without a researcher having to enumerate and >analyze the TMs themselves (i.e., build on past explorations and research).

I would too be really interested in being part of this "curating" effort. I believe that it is really needed for all of these results to gain high trust and confidence level.

Bbchallenge is an attempt that I initially scoped to be limited to questions related to BB(5) but I would be 100% be open to have it have a more general TM/BB research scope.

I believe that it would be good to think about such a platform collectively.

Many thanks for your emails,

T

[Terry Ligocki]

Yes, the RPI page and work was very much like what you've started! The problem is these efforts often grow, flourish, and then decay over 5-10 years (and are often forgotten). I would like to fix that AND recover the treasure from past efforts and put it on display with the new work. Soon, I'm going to start a discussion on where this could be done and how it could be done to guarantee longevity. One option is GitHub which is well past critical mass and will likely survive well into the future and will almost certainly have migration paths to "the next big thing".

Another connection I'd like to make is to the Santa Fe Institute Applied Complexity effort, https://www.santafe.edu/applied-complexity/office and https://www.complexityexplorer.org, which was started by some amazing people and is exploring all aspects of complexity.

There is also Scott Aaronson at UT Austin (who is a member of this discussion group and helped revive the current interest in all this) whose thoughts on all this (beyond his recent paper) would be very useful.

Finally, with the connection between the BB problem (and related questions) and Collatz-like behavior, we find ourselves intertwining two problems that students and researchers have been traditionally directed away from as traps or infinite time sinks! I feel proud to jump off the edge of the world with everyone involved in this effort...

                                Terry J. (Ligocki, tjli...@gmail.com)

P.S. Pascal and Heiner have some links to past efforts to have webpages that document some aspects of the BB problem and, in general, TMs. I haven't had a chance to check those against things on the https://bbchallenge.org page(s). I'm going to try and contact people who worked on the RPI page with the goal of piecing it back together and going from there...

You received this message because you are subscribed to the Google Groups "Busy Beaver Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to busy-beaver-dis...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/busy-beaver-discuss/8ea7f145-d29d-4b27-a408-de4f8021e310n%40googlegroups.com.

---

Look, let me explain something to you. I'm not Mr. Lebowski. You're Mr. Lebowski.
I'm the Dude. So that's what you call me. That or His Dudeness... Duder... or El Duderino,
If, you know, you're not into the whole brevity thing.

       - The Big Lebowski (Jeff Bridges)

[Heiner Marxen]

These are fascinating times :-)

From a short look into the TM definition of the Lean community I take the impression that that is a 4-tuple TM: either print or move.  Also, no halting state or halting action, just halting because of undefined transition.  But this latter deviation from our TMs is no real problem.  The former needs more work.

The optimistic view is the scientific view: finding that something does not work, is a finding, too.  Ha, I really like science.

Hold up the good work, everybody!

[Tristan Stérin]

> Yes, the RPI page and work was very much like what you've started! The problem is these efforts often grow, flourish, and then decay over 5-10 years (and are often forgotten). I would like to fix that AND recover the > treasure from past efforts and put it on display with the new work. Soon, I'm going to start a discussion on where this could be done and how it could be done to guarantee longevity. One option is GitHub which is >well past critical mass and will likely survive well into the future and will almost certainly have migration paths to "the next big thing".

I am completely on board with your concern. We don't want to perpetually re-invent the wheel on isolated islands (it is also an issue with Collatz-related research). A nice feature of GitHub/GitLab is that they allow for collaboration very easily. For instance, Shawn noticed some errors in my writing and was able to directly submit his proposed changes https://github.com/bbchallenge/bbchallenge/pull/10

Maybe we could think about organizing an online workshop/seminar with all the BB/TM-motivated people and see how we could collaboratively address this concern? What I am thinking about here is more of a meta seminar on how to curate and organize all these research efforts rather than a research seminar on recent (or not recent) developments in the field. Although I would also be very interested in the latter :D

> Hold up the good work, everybody!

Yes!!