9 ms·

With fifth busy beaver, researchers approach computation's limits

jl6 2y ago
BB(0) = 0 BB(1) = 1 BB(2) = 4 BB(3) = 6 BB(4) = 13 They just proved that BB(5) = 47,176,870. It is known that BB(6) must be at least 10^10^...^10 (a tower of exponents fifteen levels high). https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%CE%A3_and_S https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%...
- deleted 2y ago
  [deleted]
- deleted 2y ago
  [deleted]
- pdonis 2y ago
  The definitions of the "BB" function don't all appear to be the same. The article referenced in this overall discussion says BB(2) = 6. In the notation of the Wikipedia article you reference, this would be S(2) = 6; S is the number of steps. What has now been proved is that S(5) = 47,176,870. However, your BB values for 0, 1, 2, 3, and 4 match the Wikipedia article's notation for Sigma; Sigma is the number of 1s written on the tape at halting. In that notation, what has now been proved is Sigma(5) = 4098.
  - LegionMammal978 2y ago
    Yeah, this is a bit confusing, and the subject of repeated internal controversy. Most of the twentieth-century authors focused on the number of 1s, Σ(n), following Radó's original practice of treating σ(M) as the score of a machine M in the "Busy Beaver game". But when Aaronson re-popularized it in 2020 [0], he used BB(n) to denote the number of steps (which Radó called S(n)), and the bbchallenge project has been using this latter convention for publicity. Pascal Michel's website [1] has all the Σ(n) and S(n) bounds up to n = 7. Personally, I think both functions have their strengths and weaknesses. Σ(n) is easier to calculate for machines that run too long to be simulated directly (e.g., Skelet #1 from the article) but leave a known pattern on the tape, and it also has historical priority. But S(n) has a simpler argument for being undecidable, since it provides a trivial filter for testing if a candidate machine cannot halt. Also, σ(M) is a bit weird in that it has no lower bound in terms of s(M), since an adversarial machine could do a colossal amount of work before wiping its tape at the end. Regardless, past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different. (At least, the sets of champion machines aren't disjoint: Σ(5) = 4098 is shared by both the S(5) champion and another machine that runs a quarter as long.) The score of a machine is dominated by googological strength rather than technicalities in the definition. [0] https://scottaaronson.blog/?p=4916 https://scottaaronson.blog/?p=4916 [1] https://bbchallenge.org/~pascal.michel/ha https://bbchallenge.org/~pascal.michel/ha
    - pdonis 2y ago
      Thanks for this information, it's very helpful! Also I had no idea that "googological strength" was a thing. :-)
      - Sharlin 2y ago
        I'll just leave this here: https://googology.fandom.com/wiki/Googology_Wiki https://googology.fandom.com/wiki/Googology_Wiki
    - nickdrozd 2y ago
      > past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different. My feeling is that this trend cannot continue forever, and for infinitely many N they are different. If they are always the same, then you could find the steps champion just by finding the marks champion. This would be convenient, because as you pointed out, steps are more logically important, while marks are more practically important. But this feels too good to be true, and so it probably isn't.
      - LegionMammal978 2y ago
        Hmm, around n = 2 or k = 2, there are only 2 added transitions for a machine to do "the next big thing" googologically, so that doesn't leave much slack for many different machines at the same level. But maybe that could happen closer to the n = k line, where each increment adds many new transitions. Or to the contrary, maybe each increment just does several "next big things".
        cwillu 2y ago
        Or the next big things were implementable at n-3, but finally pay off at n+1?
      - lupire 2y ago
        What does "practically" mean here?
- Natsu 2y ago
  Looking at the pictures on Wikipedia regarding those programs, it's interesting how they seem to result in fractals.
  - LegionMammal978 2y ago
    This mainly has to do with the BB(5) champion having "bouncing" behavior: it moves from the left side of the current pattern to the right side and back again, each time extending it slightly. Since the time it takes to grow the pattern is strictly proportional to its current size, you end up with a bunch of parabolas that appear self-similar.
  - jerf 2y ago
    That is because these are small. Small machines can not help but still have those sorts of patterns in them. See all the simple 1-D automata of interest, for instance: https://atlas.wolfram.com/01/01/ https://atlas.wolfram.com/01/01/ As you step up I am fairly confident you'll see the winners get noisier and noisier. They'll have some sort of pattern, just ones you won't be able to comprehend. For some suitable definition of "noisier" this might even be a provable claim.
    - Natsu 2y ago
      Wouldn't it make more sense for the longest running ones to be fractal in a sense given that the self-similarity is sort of compressible? I guess we'll probably never know, because it's not clear that we'll ever find another BB winner.
    - 317070 2y ago
      Ha, the funny thing is, there are conjectures both ways! Some people think winners get noisier and noisier, the spaghetti code conjecture. Others actually think the winners get cleaner and cleaner, the clean code conjecture. Personally, I am slightly leaning towards clean code being more powerful. Chaos is hard to control. https://nickdrozd.github.io/2022/03/12/formal-theory-of-spaghetti-code.html https://nickdrozd.github.io/2022/03/12/formal-theory-of-spag...
kryptiskt 2y ago
One notable thing here is that the proof is a Coq proof. I wonder if it is the first significant proof that starts out implemented in a theorem prover, instead of being a known proof translated to such a system. Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.
- LegionMammal978 2y ago
  As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem was that the deciders and manual proofs were disorganized and somewhat suspect. The worst offenders here were Skelet #1, which needed a bespoke program to accelerate it to its ultimate pattern [0], and Skelet #17, which took Xu seven pages' worth of dense reasoning to prove non-halting [1]. The full Coq proof put a much-needed degree of confidence into these results. [0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html https://www.sligocki.com/2023/03/13/skelet-1-infinite.html [1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/184 https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
- poikroequ 2y ago
  > [The four color theorem] was the first major theorem to be proved using a computer. https://en.m.wikipedia.org/wiki/Four_color_theorem https://en.m.wikipedia.org/wiki/Four_color_theorem I guess maybe I don't understand what you mean by "formally verified setting", but I believe the four color theorem was first proven using a computer. > Although flawed, Kempe's original purported proof of the four color theorem provided some of the basic tools later used to prove it. It sounds like Kempe laid some of the groundwork, but then the theorem was ultimately proved using a computer. I could be wrong though, I'm not an expert in this area.
  - nyssos 2y ago
    The original four color theorem proof used a computer as a computational aid for some nasty casework: the procedure for checking each case and the list of cases that needed to be checked were found by hand. Proving something in a theorem prover means the proof itself is an object constructed in the prover's language.
bryan0 2y ago
Aaronson’s post on BB(5): https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088
- deleted 2y ago
  [deleted]
pvg 2y ago
Some comments on this result by Scott Aaronson https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088 And for leisure-class beavers, some big related threads from earlier this year: https://news.ycombinator.com/item?id=40453221 https://news.ycombinator.com/item?id=40453221 https://news.ycombinator.com/item?id=38113792 https://news.ycombinator.com/item?id=38113792 https://news.ycombinator.com/item?id=37910297 https://news.ycombinator.com/item?id=37910297
- inhumantsar 2y ago
  > leisure-class beavers I can't not find this phrase funny. out of context it reads like something out of Terry Pratchett or Douglas Adams.
  - IIAOPSW 2y ago
    frankly, leisure beaver sounds like a raunchy innuendo
    - labster 2y ago
      [flagged]
    - marius_gaciu 2y ago
      Vvvv
  - max-ibel 2y ago
    Exactly. Those are also not funny at all.
- deleted 2y ago
  [deleted]
deleted 2y ago
[deleted]
- deleted 2y ago
  [deleted]
cmdrriker 2y ago
[flagged]
- deleted 2y ago
  [deleted]
phaedrus 2y ago
I wrote program to solve the cutting stock problem (https://en.wikipedia.org/wiki/Cutting_stock_problem https://en.wikipedia.org/wiki/Cutting_stock_problem) for a personal project. I couldn't (or didn't want to) use any existing program for it because my stock involved cutting pieces shaped like either /---/, /---|, or |---| and I didn't want to waste material on the 45 cut. I find it interesting that the description of Brady's program to optimize search for BB(4) by cutting out search subtrees whose differences don't matter is fairly close to a description of what I did to make my program fast.
wodenokoto 2y ago
So we were just lucky that all non-halting programs of length 5 just happened to be provably non-halting?
- tromp 2y ago
  The article touches on that: > But just four days ago, mxdys and another contributor known as Racheline discovered a barrier for BB(6) that seems insurmountable: a six-rule machine whose halting problem resembles a famously intractable math problem called the Collatz conjecture. Connections between Turing machines and the Collatz conjecture date back to a 1993 paper by the mathematician Pascal Michel, but the newly discovered machine, dubbed “Antihydra,” is the smallest one that appears unsolvable without a conceptual breakthrough in mathematics.
  - dwh452 2y ago
    I'm curious how the Turing machines can resemble problems which take input? BB(n) is defined as a n-state Turing machine that starts off with an empty tape. Collatz(n) is how many steps are taken before it terminates when starting with input 'n'. Does this mean a BB(6) machine which resembles Collatz is testing all possible values as part of it program and not part of anything on the tape (since the tape start out empty)?
    - LegionMammal978 2y ago
      It's not testing all values, but one particular starting point. In all likelyhood, it will never reach its stopping condition from this starting point, but proving this even for a single value is currently intractable. Compare with the "5x + 1" variant of the Collatz cojecture, where many values are believed (but not proven) to run off to infinity, never to return.
    - srcreigh 2y ago
      Edit:nvm see thread For collatz, the empty input machine loops over all natural numbers and halts if it finds one which doesn’t eventually reach 1. To prove that it never halts, you’d have to prove the collatz conjecture. Otherwise you’d have to find the smallest counter example of the collatz conjecture.
tromp 2y ago
> There are many variants of the original busy beaver problem, and some Busy Beaver Challenge contributors plan to keep working on these. One such variant is a functional busy beaver defined in terms of the lambda calculus [1]. Since it measures program size in bits rather than states, it allows many more values to be determined (37 so far versus only 6 for TMs), and the gap between the largest known value and values beyond Graham's Number is a mere 13 program bits. A closely related variant [2] can be directly expressed in terms of Kolmogorov complexity, which Mikhail Andreev argues [3] is crucial for applications in Information Theory. [1] https://oeis.org/A333479 https://oeis.org/A333479 [2] https://oeis.org/A361211 https://oeis.org/A361211 [3] https://arxiv.org/pdf/1703.05170 https://arxiv.org/pdf/1703.05170
- passion__desire 2y ago
  Isn't there another formulation of BB where we count shifts (from left to right, and from right to left) a TM makes instead of strings of contiguous 1s. I remember seeing a video about this definition.
  - Sniffnoy 2y ago
    The variant of BB discussed in the article is counting steps, not 1s. (I guess "shifts" is equivalent to steps, although that seems like a more roundabout way of specifying it.) Also, I don't think anyone counts strings of contiguous 1s, although of course one could define such a thing.
- anandijain 2y ago
  A bit unrelated but you posted oeis so hoping you know. In the article they mention there are 17 trillion possible 5-2 turing machines. I tried finding the sequence for this but couldn't. I found this https://oeis.org/A141475 https://oeis.org/A141475, but it gives 27 trillion for 5.
  - tromp 2y ago
    While the official formula [1] is (4(n+1))^(2n) , if one ignores the symbol written and head movement for transitions to halt, then this becomes (4n+1)^(2n), which is ~ 17 trillion for n=5. [1] https://oeis.org/A052200 https://oeis.org/A052200
titanomachy 2y ago
I worked for a couple years with a formidable and incomprehensibly smart engineer who ascended the IC ranks faster than anyone I’ve seen at an elite tech company. He quit the job a few years ago, and when I asked him his plans he told me he was going to work on the busy beaver problem. I can’t help but wonder if he is mxdys, the pseudonymous contributor mentioned in the article who wrapped up the formal proof of BB(5). I’ll probably never know.
- jebarker 2y ago
  If it were them would you be surprised that they wanted to remain anonymous?
  - someplaceguy 2y ago
    I'm sorry, I don't get it. What are you suggesting to be the motivation to remain anonymous in this case?
    - DaiPlusPlus 2y ago
      Prevents embarrassment if it turns out one’s idea is wrong, I suppose.
      - someplaceguy 2y ago
        The person in question formalized the entire proof in Coq, which certifies its correctness. To me, that makes your conjecture very unlikely to be true...
    - jebarker 2y ago
      I didn't mean to suggest anything. I was just interested in whether they thought that remaining anonymous was in keeping with their ex-colleagues character. Written communication is hard!
      - deleted 2y ago
        [deleted]
ks2048 2y ago
According to Scott Aaronson's blog post on this, there are 16,679,880,978,201 5-state Turing machines. I wonder if we know what percentage of them halt? Edit: number of TM for n states: (4n + 1)^(2n). Found this (for smaller n), which is the kind of analysis I was curious about: https://github.com/LukasKalbertodt/beaver https://github.com/LukasKalbertodt/beaver
- srcreigh 2y ago
  We must know the percentage which halt! I can’t find it in the bbchallenge.org site, but every machine is categorized.
  - LegionMammal978 2y ago
    Not necessarily. The seed database only contains TMs in tree normal form (TNF), which already contains several reductions. To convert the percentage of TNF halters to the percentage of total halters, you'd have to account for the multiplicity of each TNF machine, which is a bunch of fiddly combinatorics. Also, you'd have to add the machines that have no TNF form due to never writing a 1 to the tape.
nayuki 2y ago
From the article: > To distill the essence of the halting problem into a simpler form, Radó imagined sorting Turing machines into groups based on how many rules they had — one group for all one-rule Turing machines, another for all two-rule machines, and so on. Sure, that leaves infinitely many such groups, since a Turing machine can have any number of rules. But the number of distinct machines in every group is finite, since there are only so many possible combinations of rules. > With two rules, there are already over 6,000 distinct Turing machines to consider; that number swells to millions with three rules, and to billions with four. I'm pretty sure the standard terminology is "states", not "rules". This deviation made it harder to understand. Each state produces 2 transition rules, depending on the symbol at the tape head.
- deleted 2y ago
  [deleted]
smokel 2y ago
The original Busy Beaver paper by Tibor Radó ("On Non-Computable Functions") is actually quite easy and fun to read. For a modern version of the paper with some additional notes, see https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Remastered.pdf https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
nickdrozd 2y ago
Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
- tromp 2y ago
  > the 2-color 4-state case? You mean the 2-state 4-color case...
  - nickdrozd 2y ago
    Fixed, thanks
- LegionMammal978 2y ago
  > Has anyone tried applying these same techniques to the 2-color 4-state case? I assume you mean the 4-color case. As I understand it, the deciders currently in use are sufficient to prove all the 2×4 holdouts non-halting. So the current champion gives us Σ(2,4) = 2,050 and S(2,4) = 3,932,964, barring some big errors in the decider design. The result just hasn't been organized in one place. > (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) Yes, 2×5 has the Hydra, and 6×2 has the Antihydra, which compute the same iteration, but with different starting points and halting conditions. The standard conjecture (related to Mahler's 3/2 problem) is that this iteration is uniformly distributed mod 2, and a proof of that conjecture would very likely prove both machines non-halting, by yielding suprema and infima on the cumulative ratio of 0s to 1s. But of course there is no known method of proof.
- srcreigh 2y ago
  > By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof. The year is 52,000 CE and humans have solved BB(18) in the sense of exhaustively categorizing halting vs non-halting 19-state no-input programs. They have used a proof generator based on a logical theory called Aleph*, and at that time it had been known for 1.5k years that ZFC is incapable of establishing BB(18). Compared to the year 2024 CE, considerable millennia before Aleph* came into use, it is clear that no program written at that point in history was capable of even using brute force proof checking to solve BB(18) in theory (like how we can enumerate and check ZFC proofs today to solve BB(??) in theory). That's what is meant by the "humans intuit solutions to the halting problem" position. AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. And due to BB being incomputable, humans had to develop new theory to be able to construct the programs required. Something has to be accredited for the results, and it can't be computation since the programs did not exist.
wayeq 2y ago
> "After decades of uncertainty, a motley team of programmers has proved precisely how complicated simple computer programs can get." my team has also proved this via our production codebase
- kaptainscarlet 2y ago
  These researchers clearly haven't looked at our NodeJS ERP system.
- deleted 2y ago
  [deleted]
DowsingSpoon 2y ago
Maybe I’m just an unsophisticated code monkey, but I read a little about Busy Beaver from time to time and I just don’t get it. Why is this an interesting problem? What do we hope to learn from it?
- lkuty 2y ago
  IMO, because it gives you a way to know if a program will terminate or not. If it consists of 5 states and goes beyond 47176870 steps of execution, then it will never halt. However, we are currently limited to 1 to 5 states Turing programs. And you can make correspondance between some Turing machines and some theorems in Mathematics thus it gives you a way to prove them I guess.
  - suzzer99 2y ago
    The one thing I didn't understand is the distribution 1s and 0s on the tape. Does each Turing machine have to be solved for all possible combinations of 1s and 0s?
    - ropejumper 2y ago
      The game is defined to start with an infinite all-zeroes tape.
      - chmod775 2y ago
        An important observation is that it doesn't really matter what you start with, because you have two ways to "reduce" each Turing machine to one that can start with all zeroes: - You can "flip" rules/initial tape values, trying to get a machine that can start with all 0s. This is not always possible. A trivial case where it is possible is a machine that wants to start with all 1s (just flip everything). - You can insert more rules to set the tape up as needed. This makes it an BBn+x busy beaver candidate, but at least it's not your problem at BBn now. The last way can get a bit complicated because you need to insert ad-hoc logic, since the tape is infinitely long. So it's not a just a case of inserting setup at the beginning of the program (because you can't setup an infinite tape in finite steps). Also to be fair this second point is a non-trivial assertion and requires proof that it is actually possible to do in every case. It is obviously possible to do for every machine that runs in finite steps though (since it can only consider a finite amount of tape). Luckily actual computers have finite memory which is generally initialized with 0 anyways.
seeknotfind 2y ago
Who else thinks mxdys is an AI program gone rogue? Thank you sweet mxdys!
Jean-Papoulos 2y ago
Can someone explain how there can a finite number of rules ? Could the rule "If it's a 0, change it to 1 and move 3 squares to the left" produce a different result than when moving 4 squares, or is that not the case ?
- hmry 2y ago
  You can only ever move one step to the left or right. If you want to move multiple steps, you need multiple states to use as a counter, or set up the tape a specific way ahead of time so you know when to stop moving.
- masklinn 2y ago
  A turing machine rule can only: - set the current cell’s value - move by one cell - switch to the next rule (or halt) (A TM rule has one sub-rule for each valid value / symbol) Turing machines are characterised by the number of values (or symbols) and the number of rules (or states) (and technically the number of directions but TMs are generally one-dimensional). The Busy Beaver game fixes the number of symbols to 2, and only varies the number of states e.g. BB(3) is played on 3-states 2-symbols turing machines. Thus the number of possible rules in BB(n) (n-states 2 symbols turing machine) is necessarily limited, to (4n + 4)^2n.
etx 2y ago
[dead]
lupire 2y ago
https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088 > You need to find a mathematical reason why it can’t halt, and there’s no systematic method for finding such reasons—that was the great discovery of Gödel and Turing nearly a century ago. That's only true for sufficiently large N, large enough to encode the halting paradox. (How large is that N? It's larger than 5!) Smaller N can and do fall to systematic methods. > (x) = (5x+18)/3 if x = 0 (mod 3), The second = should be \equivalent. This is a rare case where that actually matters, because is being used in both non-modular integer operations (divide by 3) and modular operations (where division by 3 is not defined).
openasocket 2y ago
All things considered, the proof is pretty short! It’s 19,000 lines of Coq (including white space and comments). And in my experience, if this were compiled into a traditional paper it would be significantly shorter than the Coq version. (Of course, length of the proof really isn’t a measure of difficulty or complexity, but it is a very rough yardstick we can use.) When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it. As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.

jl6 2y ago

BB(0) = 0 BB(1) = 1 BB(2) = 4 BB(3) = 6 BB(4) = 13 They just proved that BB(5) = 47,176,870. It is known that BB(6) must be at least 10^10^...^10 (a tower of exponents fifteen levels high). https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%CE%A3_and_S https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%...

deleted 2y ago
[deleted]
deleted 2y ago
[deleted]
pdonis 2y ago
The definitions of the "BB" function don't all appear to be the same. The article referenced in this overall discussion says BB(2) = 6. In the notation of the Wikipedia article you reference, this would be S(2) = 6; S is the number of steps. What has now been proved is that S(5) = 47,176,870. However, your BB values for 0, 1, 2, 3, and 4 match the Wikipedia article's notation for Sigma; Sigma is the number of 1s written on the tape at halting. In that notation, what has now been proved is Sigma(5) = 4098.
- LegionMammal978 2y ago
  Yeah, this is a bit confusing, and the subject of repeated internal controversy. Most of the twentieth-century authors focused on the number of 1s, Σ(n), following Radó's original practice of treating σ(M) as the score of a machine M in the "Busy Beaver game". But when Aaronson re-popularized it in 2020 [0], he used BB(n) to denote the number of steps (which Radó called S(n)), and the bbchallenge project has been using this latter convention for publicity. Pascal Michel's website [1] has all the Σ(n) and S(n) bounds up to n = 7. Personally, I think both functions have their strengths and weaknesses. Σ(n) is easier to calculate for machines that run too long to be simulated directly (e.g., Skelet #1 from the article) but leave a known pattern on the tape, and it also has historical priority. But S(n) has a simpler argument for being undecidable, since it provides a trivial filter for testing if a candidate machine cannot halt. Also, σ(M) is a bit weird in that it has no lower bound in terms of s(M), since an adversarial machine could do a colossal amount of work before wiping its tape at the end. Regardless, past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different. (At least, the sets of champion machines aren't disjoint: Σ(5) = 4098 is shared by both the S(5) champion and another machine that runs a quarter as long.) The score of a machine is dominated by googological strength rather than technicalities in the definition. [0] https://scottaaronson.blog/?p=4916 https://scottaaronson.blog/?p=4916 [1] https://bbchallenge.org/~pascal.michel/ha https://bbchallenge.org/~pascal.michel/ha
  - pdonis 2y ago
    Thanks for this information, it's very helpful! Also I had no idea that "googological strength" was a thing. :-)
    - Sharlin 2y ago
      I'll just leave this here: https://googology.fandom.com/wiki/Googology_Wiki https://googology.fandom.com/wiki/Googology_Wiki
  - nickdrozd 2y ago
    > past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different. My feeling is that this trend cannot continue forever, and for infinitely many N they are different. If they are always the same, then you could find the steps champion just by finding the marks champion. This would be convenient, because as you pointed out, steps are more logically important, while marks are more practically important. But this feels too good to be true, and so it probably isn't.
    - LegionMammal978 2y ago
      Hmm, around n = 2 or k = 2, there are only 2 added transitions for a machine to do "the next big thing" googologically, so that doesn't leave much slack for many different machines at the same level. But maybe that could happen closer to the n = k line, where each increment adds many new transitions. Or to the contrary, maybe each increment just does several "next big things".
      - cwillu 2y ago
        Or the next big things were implementable at n-3, but finally pay off at n+1?
    - lupire 2y ago
      What does "practically" mean here?
Natsu 2y ago
Looking at the pictures on Wikipedia regarding those programs, it's interesting how they seem to result in fractals.
- LegionMammal978 2y ago
  This mainly has to do with the BB(5) champion having "bouncing" behavior: it moves from the left side of the current pattern to the right side and back again, each time extending it slightly. Since the time it takes to grow the pattern is strictly proportional to its current size, you end up with a bunch of parabolas that appear self-similar.
- jerf 2y ago
  That is because these are small. Small machines can not help but still have those sorts of patterns in them. See all the simple 1-D automata of interest, for instance: https://atlas.wolfram.com/01/01/ https://atlas.wolfram.com/01/01/ As you step up I am fairly confident you'll see the winners get noisier and noisier. They'll have some sort of pattern, just ones you won't be able to comprehend. For some suitable definition of "noisier" this might even be a provable claim.
  - Natsu 2y ago
    Wouldn't it make more sense for the longest running ones to be fractal in a sense given that the self-similarity is sort of compressible? I guess we'll probably never know, because it's not clear that we'll ever find another BB winner.
  - 317070 2y ago
    Ha, the funny thing is, there are conjectures both ways! Some people think winners get noisier and noisier, the spaghetti code conjecture. Others actually think the winners get cleaner and cleaner, the clean code conjecture. Personally, I am slightly leaning towards clean code being more powerful. Chaos is hard to control. https://nickdrozd.github.io/2022/03/12/formal-theory-of-spaghetti-code.html https://nickdrozd.github.io/2022/03/12/formal-theory-of-spag...

kryptiskt 2y ago

One notable thing here is that the proof is a Coq proof. I wonder if it is the first significant proof that starts out implemented in a theorem prover, instead of being a known proof translated to such a system. Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.

LegionMammal978 2y ago
As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem was that the deciders and manual proofs were disorganized and somewhat suspect. The worst offenders here were Skelet #1, which needed a bespoke program to accelerate it to its ultimate pattern [0], and Skelet #17, which took Xu seven pages' worth of dense reasoning to prove non-halting [1]. The full Coq proof put a much-needed degree of confidence into these results. [0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html https://www.sligocki.com/2023/03/13/skelet-1-infinite.html [1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/184 https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
poikroequ 2y ago
> [The four color theorem] was the first major theorem to be proved using a computer. https://en.m.wikipedia.org/wiki/Four_color_theorem https://en.m.wikipedia.org/wiki/Four_color_theorem I guess maybe I don't understand what you mean by "formally verified setting", but I believe the four color theorem was first proven using a computer. > Although flawed, Kempe's original purported proof of the four color theorem provided some of the basic tools later used to prove it. It sounds like Kempe laid some of the groundwork, but then the theorem was ultimately proved using a computer. I could be wrong though, I'm not an expert in this area.
- nyssos 2y ago
  The original four color theorem proof used a computer as a computational aid for some nasty casework: the procedure for checking each case and the list of cases that needed to be checked were found by hand. Proving something in a theorem prover means the proof itself is an object constructed in the prover's language.

bryan0 2y ago

Aaronson’s post on BB(5): https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088

deleted 2y ago
[deleted]

pvg 2y ago

Some comments on this result by Scott Aaronson https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088 And for leisure-class beavers, some big related threads from earlier this year: https://news.ycombinator.com/item?id=40453221 https://news.ycombinator.com/item?id=40453221 https://news.ycombinator.com/item?id=38113792 https://news.ycombinator.com/item?id=38113792 https://news.ycombinator.com/item?id=37910297 https://news.ycombinator.com/item?id=37910297

inhumantsar 2y ago
> leisure-class beavers I can't not find this phrase funny. out of context it reads like something out of Terry Pratchett or Douglas Adams.
- IIAOPSW 2y ago
  frankly, leisure beaver sounds like a raunchy innuendo
  - labster 2y ago
    [flagged]
  - marius_gaciu 2y ago
    Vvvv
- max-ibel 2y ago
  Exactly. Those are also not funny at all.
deleted 2y ago
[deleted]

deleted 2y ago

[deleted]

deleted 2y ago
[deleted]

cmdrriker 2y ago

[flagged]

deleted 2y ago
[deleted]

phaedrus 2y ago

I wrote program to solve the cutting stock problem (https://en.wikipedia.org/wiki/Cutting_stock_problem https://en.wikipedia.org/wiki/Cutting_stock_problem) for a personal project. I couldn't (or didn't want to) use any existing program for it because my stock involved cutting pieces shaped like either /---/, /---|, or |---| and I didn't want to waste material on the 45 cut. I find it interesting that the description of Brady's program to optimize search for BB(4) by cutting out search subtrees whose differences don't matter is fairly close to a description of what I did to make my program fast.

wodenokoto 2y ago

So we were just lucky that all non-halting programs of length 5 just happened to be provably non-halting?

tromp 2y ago
The article touches on that: > But just four days ago, mxdys and another contributor known as Racheline discovered a barrier for BB(6) that seems insurmountable: a six-rule machine whose halting problem resembles a famously intractable math problem called the Collatz conjecture. Connections between Turing machines and the Collatz conjecture date back to a 1993 paper by the mathematician Pascal Michel, but the newly discovered machine, dubbed “Antihydra,” is the smallest one that appears unsolvable without a conceptual breakthrough in mathematics.
- dwh452 2y ago
  I'm curious how the Turing machines can resemble problems which take input? BB(n) is defined as a n-state Turing machine that starts off with an empty tape. Collatz(n) is how many steps are taken before it terminates when starting with input 'n'. Does this mean a BB(6) machine which resembles Collatz is testing all possible values as part of it program and not part of anything on the tape (since the tape start out empty)?
  - LegionMammal978 2y ago
    It's not testing all values, but one particular starting point. In all likelyhood, it will never reach its stopping condition from this starting point, but proving this even for a single value is currently intractable. Compare with the "5x + 1" variant of the Collatz cojecture, where many values are believed (but not proven) to run off to infinity, never to return.
  - srcreigh 2y ago
    Edit:nvm see thread For collatz, the empty input machine loops over all natural numbers and halts if it finds one which doesn’t eventually reach 1. To prove that it never halts, you’d have to prove the collatz conjecture. Otherwise you’d have to find the smallest counter example of the collatz conjecture.

tromp 2y ago

> There are many variants of the original busy beaver problem, and some Busy Beaver Challenge contributors plan to keep working on these. One such variant is a functional busy beaver defined in terms of the lambda calculus [1]. Since it measures program size in bits rather than states, it allows many more values to be determined (37 so far versus only 6 for TMs), and the gap between the largest known value and values beyond Graham's Number is a mere 13 program bits. A closely related variant [2] can be directly expressed in terms of Kolmogorov complexity, which Mikhail Andreev argues [3] is crucial for applications in Information Theory. [1] https://oeis.org/A333479 https://oeis.org/A333479 [2] https://oeis.org/A361211 https://oeis.org/A361211 [3] https://arxiv.org/pdf/1703.05170 https://arxiv.org/pdf/1703.05170

passion__desire 2y ago
Isn't there another formulation of BB where we count shifts (from left to right, and from right to left) a TM makes instead of strings of contiguous 1s. I remember seeing a video about this definition.
- Sniffnoy 2y ago
  The variant of BB discussed in the article is counting steps, not 1s. (I guess "shifts" is equivalent to steps, although that seems like a more roundabout way of specifying it.) Also, I don't think anyone counts strings of contiguous 1s, although of course one could define such a thing.
anandijain 2y ago
A bit unrelated but you posted oeis so hoping you know. In the article they mention there are 17 trillion possible 5-2 turing machines. I tried finding the sequence for this but couldn't. I found this https://oeis.org/A141475 https://oeis.org/A141475, but it gives 27 trillion for 5.
- tromp 2y ago
  While the official formula [1] is (4(n+1))^(2n) , if one ignores the symbol written and head movement for transitions to halt, then this becomes (4n+1)^(2n), which is ~ 17 trillion for n=5. [1] https://oeis.org/A052200 https://oeis.org/A052200

titanomachy 2y ago

I worked for a couple years with a formidable and incomprehensibly smart engineer who ascended the IC ranks faster than anyone I’ve seen at an elite tech company. He quit the job a few years ago, and when I asked him his plans he told me he was going to work on the busy beaver problem. I can’t help but wonder if he is mxdys, the pseudonymous contributor mentioned in the article who wrapped up the formal proof of BB(5). I’ll probably never know.

jebarker 2y ago
If it were them would you be surprised that they wanted to remain anonymous?
- someplaceguy 2y ago
  I'm sorry, I don't get it. What are you suggesting to be the motivation to remain anonymous in this case?
  - DaiPlusPlus 2y ago
    Prevents embarrassment if it turns out one’s idea is wrong, I suppose.
    - someplaceguy 2y ago
      The person in question formalized the entire proof in Coq, which certifies its correctness. To me, that makes your conjecture very unlikely to be true...
  - jebarker 2y ago
    I didn't mean to suggest anything. I was just interested in whether they thought that remaining anonymous was in keeping with their ex-colleagues character. Written communication is hard!
    - deleted 2y ago
      [deleted]

ks2048 2y ago

According to Scott Aaronson's blog post on this, there are 16,679,880,978,201 5-state Turing machines. I wonder if we know what percentage of them halt? Edit: number of TM for n states: (4n + 1)^(2n). Found this (for smaller n), which is the kind of analysis I was curious about: https://github.com/LukasKalbertodt/beaver https://github.com/LukasKalbertodt/beaver

srcreigh 2y ago
We must know the percentage which halt! I can’t find it in the bbchallenge.org site, but every machine is categorized.
- LegionMammal978 2y ago
  Not necessarily. The seed database only contains TMs in tree normal form (TNF), which already contains several reductions. To convert the percentage of TNF halters to the percentage of total halters, you'd have to account for the multiplicity of each TNF machine, which is a bunch of fiddly combinatorics. Also, you'd have to add the machines that have no TNF form due to never writing a 1 to the tape.

nayuki 2y ago

From the article: > To distill the essence of the halting problem into a simpler form, Radó imagined sorting Turing machines into groups based on how many rules they had — one group for all one-rule Turing machines, another for all two-rule machines, and so on. Sure, that leaves infinitely many such groups, since a Turing machine can have any number of rules. But the number of distinct machines in every group is finite, since there are only so many possible combinations of rules. > With two rules, there are already over 6,000 distinct Turing machines to consider; that number swells to millions with three rules, and to billions with four. I'm pretty sure the standard terminology is "states", not "rules". This deviation made it harder to understand. Each state produces 2 transition rules, depending on the symbol at the tape head.

deleted 2y ago
[deleted]

smokel 2y ago

The original Busy Beaver paper by Tibor Radó ("On Non-Computable Functions") is actually quite easy and fun to read. For a modern version of the paper with some additional notes, see https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Remastered.pdf https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...

nickdrozd 2y ago

Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.

tromp 2y ago
> the 2-color 4-state case? You mean the 2-state 4-color case...
- nickdrozd 2y ago
  Fixed, thanks
LegionMammal978 2y ago
> Has anyone tried applying these same techniques to the 2-color 4-state case? I assume you mean the 4-color case. As I understand it, the deciders currently in use are sufficient to prove all the 2×4 holdouts non-halting. So the current champion gives us Σ(2,4) = 2,050 and S(2,4) = 3,932,964, barring some big errors in the decider design. The result just hasn't been organized in one place. > (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.) Yes, 2×5 has the Hydra, and 6×2 has the Antihydra, which compute the same iteration, but with different starting points and halting conditions. The standard conjecture (related to Mahler's 3/2 problem) is that this iteration is uniformly distributed mod 2, and a proof of that conjecture would very likely prove both machines non-halting, by yielding suprema and infima on the cumulative ratio of 0s to 1s. But of course there is no known method of proof.
srcreigh 2y ago
> By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof. The year is 52,000 CE and humans have solved BB(18) in the sense of exhaustively categorizing halting vs non-halting 19-state no-input programs. They have used a proof generator based on a logical theory called Aleph*, and at that time it had been known for 1.5k years that ZFC is incapable of establishing BB(18). Compared to the year 2024 CE, considerable millennia before Aleph* came into use, it is clear that no program written at that point in history was capable of even using brute force proof checking to solve BB(18) in theory (like how we can enumerate and check ZFC proofs today to solve BB(??) in theory). That's what is meant by the "humans intuit solutions to the halting problem" position. AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. And due to BB being incomputable, humans had to develop new theory to be able to construct the programs required. Something has to be accredited for the results, and it can't be computation since the programs did not exist.

wayeq 2y ago

> "After decades of uncertainty, a motley team of programmers has proved precisely how complicated simple computer programs can get." my team has also proved this via our production codebase

kaptainscarlet 2y ago
These researchers clearly haven't looked at our NodeJS ERP system.
deleted 2y ago
[deleted]

DowsingSpoon 2y ago

Maybe I’m just an unsophisticated code monkey, but I read a little about Busy Beaver from time to time and I just don’t get it. Why is this an interesting problem? What do we hope to learn from it?

lkuty 2y ago
IMO, because it gives you a way to know if a program will terminate or not. If it consists of 5 states and goes beyond 47176870 steps of execution, then it will never halt. However, we are currently limited to 1 to 5 states Turing programs. And you can make correspondance between some Turing machines and some theorems in Mathematics thus it gives you a way to prove them I guess.
- suzzer99 2y ago
  The one thing I didn't understand is the distribution 1s and 0s on the tape. Does each Turing machine have to be solved for all possible combinations of 1s and 0s?
  - ropejumper 2y ago
    The game is defined to start with an infinite all-zeroes tape.
    - chmod775 2y ago
      An important observation is that it doesn't really matter what you start with, because you have two ways to "reduce" each Turing machine to one that can start with all zeroes: - You can "flip" rules/initial tape values, trying to get a machine that can start with all 0s. This is not always possible. A trivial case where it is possible is a machine that wants to start with all 1s (just flip everything). - You can insert more rules to set the tape up as needed. This makes it an BBn+x busy beaver candidate, but at least it's not your problem at BBn now. The last way can get a bit complicated because you need to insert ad-hoc logic, since the tape is infinitely long. So it's not a just a case of inserting setup at the beginning of the program (because you can't setup an infinite tape in finite steps). Also to be fair this second point is a non-trivial assertion and requires proof that it is actually possible to do in every case. It is obviously possible to do for every machine that runs in finite steps though (since it can only consider a finite amount of tape). Luckily actual computers have finite memory which is generally initialized with 0 anyways.

seeknotfind 2y ago

Who else thinks mxdys is an AI program gone rogue? Thank you sweet mxdys!

Jean-Papoulos 2y ago

Can someone explain how there can a finite number of rules ? Could the rule "If it's a 0, change it to 1 and move 3 squares to the left" produce a different result than when moving 4 squares, or is that not the case ?

hmry 2y ago
You can only ever move one step to the left or right. If you want to move multiple steps, you need multiple states to use as a counter, or set up the tape a specific way ahead of time so you know when to stop moving.
masklinn 2y ago
A turing machine rule can only: - set the current cell’s value - move by one cell - switch to the next rule (or halt) (A TM rule has one sub-rule for each valid value / symbol) Turing machines are characterised by the number of values (or symbols) and the number of rules (or states) (and technically the number of directions but TMs are generally one-dimensional). The Busy Beaver game fixes the number of symbols to 2, and only varies the number of states e.g. BB(3) is played on 3-states 2-symbols turing machines. Thus the number of possible rules in BB(n) (n-states 2 symbols turing machine) is necessarily limited, to (4n + 4)^2n.

etx 2y ago

[dead]

lupire 2y ago

https://scottaaronson.blog/?p=8088 https://scottaaronson.blog/?p=8088 > You need to find a mathematical reason why it can’t halt, and there’s no systematic method for finding such reasons—that was the great discovery of Gödel and Turing nearly a century ago. That's only true for sufficiently large N, large enough to encode the halting paradox. (How large is that N? It's larger than 5!) Smaller N can and do fall to systematic methods. > (x) = (5x+18)/3 if x = 0 (mod 3), The second = should be \equivalent. This is a rare case where that actually matters, because is being used in both non-modular integer operations (divide by 3) and modular operations (where division by 3 is not defined).

openasocket 2y ago

All things considered, the proof is pretty short! It’s 19,000 lines of Coq (including white space and comments). And in my experience, if this were compiled into a traditional paper it would be significantly shorter than the Coq version. (Of course, length of the proof really isn’t a measure of difficulty or complexity, but it is a very rough yardstick we can use.) When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it. As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.