Life, blogging, and the Busy Beaver function go on

Update (July 11): If you’re interested in blogging about progress in science and technology, check out a new fellowship from The Roots of Progress (h/t Jason Crawford).

Update (July 10): Speaking of the Busy Beaver function, check out this beautifully-produced YouTube video about BB by Duane Rich—a video that Duane says was directly inspired by my survey article! Duane tells me that a Part II is coming as well.

Update (July 7): My UT colleague David Zuckerman asked me to advertise that the FOCS Test of Time Award is urgently seeking nominations. This is your chance to get your favorite papers from 1993, 2003, or 2013 recognized!

This is my first post in well over a month. The obvious excuse is that I’ve been on a monthlong family world tour, which took me first to the Bay Area, then NYC, then Israel, then Orlando for STOC/FCRC as well as Disney World, now the Jersey Shore, and later today, back to the Bay Area, joining Dana there, and leaving the kids with my parents for a few weeks. I’ll return to Austin in mid-August, by which point, the “heat dome” will hopefully have dissipated, leaving temperatures a mere 100F or less.

I’m trying to get back into production mode. Part of that is contemplating the future of this blog, about which I’ll say more in a future post.

For now, just to wet my toes, here are three updates about the Busy Beaver function:

  • Johannes Riebel, an undergraduate at the University of Augsburg in Germany, has produced a tour-de-force bachelor’s thesis that contains, among other things, the first careful writeup of Stefan O’Rear’s result from six years ago that the value of BB(748) is independent of the ZFC axioms of set theory. Regular readers might recall that O’Rear’s result substantially improved over the initial result by me and Adam Yedidia, which showed the value of BB(8000) independent of ZFC assuming the consistency of a stronger system. Along the way, Riebel even gets a tiny improvement, showing that BB(745) independent of ZFC.
  • Pascal Michel, who curated arguably the Internet’s most detailed source of information on the Busy Beaver function, has retired from academia, and his website was at imminent risk of being lost forever. Fortunately, friends intervened and his site is now available at
  • Shawn Ligocki and Pavel Kropitz have continued to find busier beavers, with spectacular recent progress over the past couple months for Turing machines with more than 2 symbols per tape square. See here for example.

Anyway, more coming soon!

93 Responses to “Life, blogging, and the Busy Beaver function go on”

  1. David G Says:

    This seems like a perfect opportunity to bring up a question I’ve been waiting for Scott to address since the recent Quanta article about this, and I wonder if it is related: Leonard Susskind and other black hole theorists have been raising intriguing questions. Is it possible that the way that black hole volumes grow is related to the Busy Beaver function? At any rate, I’d love to hear Scott’s feedback on the Quanta article, since Scott has been dismissive of the recent claims of black holes simulated on quantum computers, but it sounds like Leonard is actually claiming that a simulated black hole is a real black hole. I know nothing about this, but I’d love to hear Scott’s opinion.

  2. Anon Says:

    As a Bay Area community college instructor of CS whose intro course builds up to undecidability and the halting and BB problems as a climax, I can’t wait to dig into this. Cheers, Scott, and I hope you’re well.

  3. Nick Drozd Says:

    A little context for the recent BB records:

    Back in 2020 when Scott wrote his survey, the 6-state 2-color record was 10^36534. That record, set by Pavel Kropitz, had stood since 2010. The 7-state 2-color record was 10^10^10^10^something. That record was established by modifying the champion program of Kropitz. (That is, it was constructed, rather than discovered.)

    Something that one might have expected at that time was that the 6-state record would be an exponential-scale number and the 7-state record would be a tetrational-scale number (where tetration is repeated exponentiation).

    But, that would have been totally wrong. In summer 2022, Shawn Ligocki found the first tetrational 6-state program, and Kropitz soon followed with a better one. The 6-state 2-color record is now ~10^^15. The previous 7-state record has been superseded.

    Part of the fun of the Busy Beaver function is that it, since it not amenable to mathematical analysis, it takes on an empirical quality. It is possible to make predictions that are falsifiable or (in a limited sense) verifiable. Here is something Scott said in his survey:

    If we draw the Busy Beavers and current Busy Beaver candidates for n ≤ 6 as directed graphs, with the n states as vertices and the 2n transitions as edges, we find that all are strongly connected : that is, every state (including the initial state) is reachable from every other state via some sequence of symbols. By contrast, the n = 7 candidate found by “Wythagoras” does not have this property, as the initial state is never revisited. But, partly for that reason, the n = 7 candidate seems clearly suboptimal.

    This turned out to be a correct prediction.

    Scott’s survey dealt exclusively with the N-state 2-color problem. But it is also possible to consider 2-state K-color. At the time of the survey, the 2-state 6-color record was 10^9866, less than the 6-state 2-color record. But there was compelling evidence to suggest that BB(N, 2) ≤ BB(2, N) for all N. So one might have conjectured that, despite appearances, the 2-state 6-color record could be improved substantially.

    That conjecture also turned to be true. Just a few months ago Ligocki found the first tetrational-scale 2-state 6-color program. And then, like clockwork, Kropitz found a better one. Now it looks like BB(6, 2) < BB(2, 6), as would be expected.

    There is perhaps a general lesson here: predictions that the current records are suboptimal are usually correct. Everybody knows that it’s an uncomputably fast-growing function, but it’s all too easy to underestimate how fast that really is. I mean, these values really get out of hand. Tetrational-scale numbers can’t be represented directly in a computer’s memory; they can only be considered obliquely with algebraic notation (look at Shawn Ligocki’s blog for details).

    And there is another lesson: constructing a champion will never work. The 7-state Wythagoras program was constructed on the basis of a program discovered by Kropitz. And it turned out to be terrible! The earliest BB records were set by Milton Green back in the 60s. He worked out a clever recursive method for constructing new programs. But all of those records have been blown away.

    With all this in mind, I think this 745-state record for undecidability is comically high. The real number is probably more like 10, maybe even lower. The current approach AIUI is to write out an interpreter in a high-level language and then compile down to TM code. That method was great for establishing some kind of bound, but it has no chance at all of getting even close to the real number. Not that I have any better ideas!

  4. Matt Says:

    Hi Scott,

    This article crossed my feed the other day: I thought it was an eloquent articulation of the experience you described back in 2015, and I’m curious if it resonates with you at all.

  5. Scott Says:

    David G #1: Can you give me a link to the Quanta article? I’m not sure which one you have in mind.

    We know from GR that the volume of a black hole just grows like the cube of its mass. I confess that I don’t see any connection here to the BB function–though if someone said what they thought the connection was, I might be able to comment.

    To be clear: we might someday learn something new by simulating (theoretical models of) tiny black holes on quantum computers. So far, we’ve learned nothing whatsoever that we didn’t already know from simulating the same models on classical computers. And also, a computer simulation of a black hole (whether classical or quantum) doesn’t satisfy extremely basic properties that a person on the street would expect from “black holes.” For example, you can’t fall into one, unless you yourself are in the simulation! None of this should be controversial.

  6. Scott Says:

    Matt #4: I mean, sure it “resonates,” insofar as it makes similar points to the ones I made 8 years ago. I don’t like the piece’s vulgarity, and I also don’t like its centering the grievances of guys who lash out with hateful misogyny, rather than guys who don’t (but who, as the world saw in 2015, are condemned all the same for any attempt, however qualified and cautious, to talk about the problem).

    The key additional factor, in my case, was that at the exact same time that I was getting clearer and clearer feedback from the dating and elite culture worlds that I was disposable, worthless, a freak, etc. etc., I was also getting clearer and clearer feedback from the academic science world that I was a budding star and that my life was special and valuable. The juxtaposition between these two messages was sharp enough to rip someone apart, and the central problem I had to solve in life was to transfer a sense of self-worth from the one world to the other. I imagine that I’ll continue till my death to try to explain what that was like, since it’s now seared in my consciousness forever, and putting it into words is probably the main thing I have to offer to the understanding of what it is to be human.

  7. Kevin Says:

    I must say, I found that bachelor’s thesis shockingly accessible. I went into that document rather surprised to hear that specific busy beaver numbers would be independent of ZFC, but the abstract alone was enough to convince me that their argument is (probably) correct.

    Nick Drozd #3: I agree that their bound is probably not a tight bound. What I wonder about is whether the Gödelian “TM that enumerates the proofs until it proves 0 = 1” can be further golfed to a lower number of states, or if they’re going to have to come up with something more elegant than that. I would tend to bet that you can find a simpler ZFC-independent TM, but it’s probably harder to prove that it’s ZFC-independent. On the other hand, code golfing has diminishing returns after a certain point, and we’re probably going to hit it relatively soon, if we’re not already there.

  8. JB Says:

    Something I’ve wondered about the BB and ZFC thing but have never been good enough at logic/foundations to know: can we just keep adding big ordinals to ZFC to be able to prove bigger and bigger BB values, or is there some limit. Surely there must be a limit I feel or else it somehow it would run into halting problem issues, or maybe the question isn’t well posed.

  9. shion_arita Says:

    I’ve been thinking about the ZFC BB result, and I’d like to see if people think I’m on the right track.

    It appears to me that, basically, BB(745) (or something lower) is independent of ZFC because… for some of the TMs that do not halt, it is unprovable that they don’t halt?

    This is kind of interesting. It relates to something that I have been thinking about relating to BB, and BBB. I was wondering whether we knew of any TMs that don’t halt, and also don’t stabilize into any kind of repetitive behavior, or some kind of nested or fractal behavior that’s otherwise predictable. I conjectured that this is true. And then I thought that for some of these machines, it’s probably not provable that this is the case for them, since they could have an arbitrarily long ‘transient’ before stabilizing to simple behavior. Let’s call such TMs chaotic nonhalting TMs.

    It appears that from the BB(745) result, this conjecture is true?

    additionally, I’ll introduce the converse as a conjecture, that if for some n, there is an n-state machine that is chaotic-nonhalting, then BB(n) is independent of ZFC.

    Unfortunately we may not get very far on this because I suspect that the chaotic-nonhaltingness of a TM is at least sometimes not provable.

  10. Bram Cohen Says:

    Nick Drozd #3:

    Indeed. In fact as BB numbers go up they probably rapidly become independent of all manner of extremely powerful axioms beyond a long list of ‘this TM never halts’

  11. Michel Says:

    What strikes me as humorous is that you dub bringing a BB number down from 748 to 745 a ‘minor’ improvement. I wonder how many orders of magnitude (or even tetration levels) lie between BB(748) and BB(745) considering the enourmous speed with which BB(x) grows.

  12. David G Says:

    Scott #5: Well, actually it is a Quanta video; the youtube link is . I guess it is clearly not a Busy Beaver connection. I have had the same understanding you articulated that these “simulated” black holes are really more of just an elaboration of quantum teleportation, but in the video Leonard seems to take the stronger position that there is a deeper reality to these simulated black holes.

  13. David G Says:

    Scott #5: Just to save you some filler time in that quanta video, you can skip the first 10 minutes.

  14. David G Says:

    Scott #5: Argg, another quanta video is involved in my impressions about this. I hope I’m not conflating them too much.

  15. Dimitris Papadimitriou Says:

    Scott #5
    The internal ( maximal) volume of a black hole grows linearly in time like ΔV~(M^2)Δυ , where Δυ approximates the age of the black hole according to external asymptotic observers.
    So , near the end of the Hawking evaporation ( nearly full evaporation time Δυ ~{M^3} in geometrized units), the maximal internal volume ( of the trapped region) is expected to be of order ( M^5 ).
    Assuming of course that the mass of the hole reaches a maximum of order M sometime, near the middle of the hole ‘s history.

  16. Gabriel Says:

    Here’s my contribution to the discussion: A cute video of a beaver that’s busy in quite an unusual way

    Scott, you said you’re moving your discussions to Facebook. That sounds interesting. What about accepting my frienship request that’s waiting there for a long time?

  17. Timothy Chow Says:

    Very nice bachelor’s thesis! I have a technical question. Has the consistency strength of the result really been lowered from SRP to ZFC?

  18. Scott Says:

    JB #8:

      Something I’ve wondered about the BB and ZFC thing but have never been good enough at logic/foundations to know: can we just keep adding big ordinals to ZFC to be able to prove bigger and bigger BB values, or is there some limit.

    Excellent question! The rather unsatisfying answer is basically: “yes, provided that we get to define the large ordinals via Turing machines—but in that case, the Turing machines could also ‘cheat’ by encoding the relevant BB values directly.” Turing himself worked all this out in his 1939 PhD thesis, shortly before he went to Bletchley Park. For more, see for example this old blog post of mine, or Section 2 of my BB survey.

  19. Scott Says:

    shion_arita #9: The way the value of BB(745) is proved independent of ZFC, is by explicitly constructing a 745-state Turing machine that halts iff it finds an inconsistency in ZFC. To date, we don’t know any better method than that one.

    Regarding your conjecture, the real crux is the definition of “chaotic nonhalting.” As an example, the 4-state Busy Beaver already seems kind of “chaotic” in its behavior, yet it’s been proven that BB(4)=107.

  20. Scott Says:

    Michel #11:

      What strikes me as humorous is that you dub bringing a BB number down from 748 to 745 a ‘minor’ improvement. I wonder how many orders of magnitude (or even tetration levels) lie between BB(748) and BB(745) considering the enourmous speed with which BB(x) grows.

    An unbelievably immense number, of course! What’s relevant is that, to achieve the lowering, Riebel “just” needed to shave 3 states off the particular 748-state Turing machine constructed by O’Rear.

  21. Scott Says:

    David G #12:

      but in the video Leonard seems to take the stronger position that there is a deeper reality to these simulated black holes.

    Indeed, that’s Lenny’s position, which I confess that I don’t share. At the least, before popping any champagne, I’d like to wait for quantum simulations whose outputs we don’t already know before we run them, and/or that push some interesting technological frontier.

  22. Scott Says:

    Gabriel #16: Done.

  23. Scott Says:

    Timothy Chow #17: Yes.

  24. Geoffrey Irving Says:

    One fun thing to estimate is how many (correct) papers of the form “BB(n) is independent of ZFC, beating the previous record” that there will ever be. The number is of course bounded above by 745, but presumably it is much lower than that because (1) papers can jump down by more than 1 and (2) there will be some n’s where BB(n) is independent of ZFC but where “BB(n) is independent of ZFC” is also independent of ZFC. My guess is <50 such papers?

  25. William Gasarch Says:

    What is known about BB(n) being ind of PA? other weaker systerms?

  26. Matt Says:

    Hey Scott,

    I’m a little confused by your take that the piece is excessively “vulgar.” I didn’t think it was particularly vulgar, so I’m curious if you could point out some examples to show what you mean. In any case, he’s describing a very visceral experience, so I think visceral language is called for.

    Surely, you would be worse off if you didn’t have the academic praise and accomplishments to fall back on? Most of these young guys experienced all the pain and suffering you did surrounding dating/sex, but they also have no meaningful career either, no accomplishments, no praise in any other areas of their lives. Isn’t that even worse than what you experienced? Weren’t you lucky to have an outlet you were actually successful in? If you didn’t discover theoretical computer science or you didn’t have the rare logical/analytical/mathematical skills to pursue that field, if you had no academic/career success or accomplishments and all you knew in every area of your life was failure, disgust, loneliness—couldn’t you have ended up as one of the “hate nerds?” What would you even do with yourself if you didn’t have STEM?

  27. Scott Says:

    William Gasarch #25: I explicitly raised that as an open problem in my survey! But I don’t know of any progress on it. I think it’s extremely plausible that BB(n) could be proved independent of PA for n much smaller than 745.

  28. Ilio Says:

    Geoffrey Irving #24,

    You meant 42, right? Beside the humour, is it actually possible for a BB(n) to be independent of ZFC without having « BB(n) is independent of ZFC » being also independent of ZFC?

  29. Emilio Says:

    Scott 19, you’re actually wrong about this. The Busy Beaver function, BB(n), does not demonstrate or prove independence from ZFC, nor does it operate as you’ve described. Instead, BB(n) corresponds to the maximum number of steps that a halting Turing machine with n states can make before it stops. The challenge of BB(n) and why it surpasses the computational capacities of systems like ZFC is due to the fact that the sequence grows incredibly fast – it outpaces any computable function and quickly reaches values that are far larger than can be handled even with the power of systems like ZFC.

    The way you’ve described the BB(745) function suggests a misunderstanding of the relationship between the Busy Beaver function and formal systems such as ZFC. BB(745) wouldn’t be used to find an inconsistency in ZFC – rather, determining the value of BB(745) is known to be an undecidable problem, even in powerful systems such as ZFC. This is due to the nature of the Busy Beaver function itself and its incredibly fast growth rate, which outstrips the capabilities of any computable function or formal system.

    Regarding your conjecture about “chaotic nonhalting”, this is also a bit of a misunderstanding. The term “chaotic” isn’t formally used in this context. When we talk about Turing machines, they either halt or don’t halt – and proving whether an arbitrary Turing machine halts is known to be an undecidable problem (the Halting Problem). The behavior of the machine may seem unpredictable or complex, but it doesn’t introduce any new category like “chaotic nonhalting”. As you noted, BB(4) is proven to be 107, which just refers to the number of steps the most ‘busy’ 4-state Turing machine makes before it halts. It doesn’t have anything to do with the machine’s behavior being “chaotic”.

  30. JB Says:

    Is there some maximum BB(n) that can be proven in any axiomatic system? My understanding is that we can easily get more powerful systems by appending big ordinals (though I’m out of my depth here I admit).

  31. Scott Says:

    Emilio #29: Your comment shows possible signs of being written by a Large Language Model. It has the external form of calling me out on errors, but then it doesn’t actually identify a single error in what I wrote; instead, it just recites some elementary facts about the BB function as if I and everyone else who’s worked on this topic didn’t know them.

    You are banned from further participation in this blog.

  32. Disney dude Says:

    How was disneyworld? Did you check out the star wars land (galaxy’s edge) at hollywood studios? It’s a very cool experience. Did you have a chance to visit the harry potter world at universal?

  33. Scott Says:

    JB #30: Yes, for every fixed axiomatic system F, there’s a maximum k such that F can prove the value of BB(k). The more powerful the axiomatic system, the larger this k can be. See my survey for more!

  34. Scott Says:

    Disney dude #32: I enjoyed Disney! The rides were pretty good—they better have been, given the hassle and expense of getting to them. 🙂 EPCOT was my favorite, just as it was when I was a child myself.

    Yes, we went on one very well-designed Star Wars ride at Hollywood Studios, though we were limited by what our 10-year-old and especially 6-year-old were willing to do.

    The hardest part was getting our 6-year-old to walk between the rides, given the crowds and long distances and heat and occasional rainstorms. He repeatedly asked to go back to the hotel room so he could play on his iPad. Having said that, while on many rides, he grudgingly admitted they were much more fun than the iPad. Understand that it takes literal Disney World to wring such a confession from him.

    No, we didn’t do Universal Studios on this trip. We took the kids to Harry Potter World on a previous trip. I liked Disney better.

  35. JimV Says:

    Matt @ #28, to me a nerd with no accomplishments is pretty close to an oxymoron. Maybe language has moved on from me again, but in my day a nerd spent a lot of time with a nose in a book, got good grades in school, and could get a technical job of some kind after graduating. I’ll grant you that most of us don’t fully live up to our potential. Maybe there is more of that now due to the high cost of college these days.

    As I see it, there is no good technical solution other than ways of learning to live with the situation, because the planet has too many people in it already. Not contributing to over-population is a bit of an accomplishment, or so I tell myself.

  36. Shion Arita Says:


    Yes, I understand that the 745 TM was explicitly constructed. To make sure I’m getting it right: iff ZFC is consistent, it will not halt. Since ZFC can’t prove that it is consistent, it can’t prove that the TM will not halt.

    Let me try for a better definition. Apologies if I’m not getting all the terminology quite right.

    I’ll have to look at what the BB(4) machine does, but maybe I would call that TM and ones like it ‘chaotic-halting’.

    a TM is chaotic-nonhalting if:

    -it does not halt
    -given some n, there is no algorithm which will give the state of the machine after n steps whose complexity class is slower growing than O(n). (in other words, there’s no way to ‘beat the TM’ in terms of knowing what it will do. As an example, one way in which a TM could be ‘beatable’ is if it ends up repeating some sequence of states in a loop.)

    the conjecture is: if given a TM, the abovie conditions are true (possibly some others are required), you can’t prove that such a TM does not halt.

    If it’s false, a possibly weaker version of it might be true, that excludes some other cases that I haven’t thought of that would allow you to prove that the TM doesn’t halt.

    Actually I’m a little less confident about the conjecture now, because there might be some weird ways that you could prove that such a ‘non-compressible’ TM will halt, but that’s not really clear to me. I do think it’s kind of a significant question though.

    As for the bounds on BB’s independence from ZFC, I have to say I would not be very surprised if BB(5) were independent of ZFC.

  37. ZFC? Says:

    What does independent of ZFC mean? Does it mean under Church Turing hypothesis we cannot compute it or something unrelated to this hypothesis?

  38. Jon Lennox Says:

    Shion Arita@36: wouldn’t a TM to calculate the digits of pi (or any other irrational number) satisfy your definition of chaotic-nonhalting?

  39. Ajit R. Jadhav Says:

    Dear Scott,

    At the infima, I wish [Prof. Dr.] David Zuckerman sufficiently well that he carry the said initiative into the 2026-end. Also this blog of yours.

    More, later… of course.


  40. Manu Says:

    This is a question I have thought for a while, and maybe some “busy-beavorologist” here can answer: Why is the study of Busy Beavers done in Turing Machines instead of, say, register machines or something alike? I know that TMs are more canonical and that all of this is done just for fun, but still. A register machine pseudocode is like real code, and much easier to understand than a TM transition table.

  41. Clade Says:

    I’m shocked that you enjoyed Disney more than Universal. I visited a Disney park recently and it was a miserable experience. Ticket prices were way too high, like 200 bucks a person high, obviously all the food and merch inside the park is insanely overpriced, and everything is done on the app now (Genie+). Everything requires a reservation on the app. It was insanely crowded and the wait times were way too long. You needed to pay extra money to go on the star wars ride, like 25 bucks a person, or else brave the three hour line.

    Universal, on the other hand, was cheaper, way shorter lines, and no app bullshit. Did you see the Hogsmeade land or the Diagon Alley land? I’d recommend the Diagon alley land, they have a ride in the gringotts bank that is fun.

    Was the star wars ride you went on Rise of the Resistance? Did you get to go on the guardians of the galaxy ride at Epcot?

  42. Adam Treat Says:


    What does the smallest busy beaver independent of ZFC and assuming the physical church Turing thesis imply about the limit of information in the universe? Like, is there an upper bound on number of bits in universe given by this number if you consider the physical church Turing thesis true?


  43. Scott Says:

    Shion Arita #36: Your conjecture is false, under any reasonable interpretation of “give the state of the machine” (even though it’s nontrivial to say what that means, in such a way that neither all nor no n-bit strings output by small, known Turing machines are “compressible” in o(n) time). For example, we could have a machine that dovetails over all other machines, or engages in any other infinite “chaotic” behavior that’s either provably “incompressible” beyond a constant factor or that you would agree is almost certainly incompressible—and proving that the machine never halts could be as simple as observing that it doesn’t contain a “halt” state.

  44. Scott Says:

    ZFC? #37: A statement is independent of ZFC if it can neither be proved nor disproved from the axioms of Zermelo-Fraenkel set theory plus the axiom of choice (though for arithmetical statements, like “this Turing machine halts,” the axiom of choice is known to be irrelevant). This is different from (and historically prior to) the concept of Church-Turing computability, which applies to problems (infinite lists of yes-or-no questions) or real numbers rather than individual statements.

  45. Scott Says:

    Manu #40: See Section 1.1 of my survey, which directly addresses your question. You can define a Busy Beaver function for any Turing-universal programming language of your choice—but to play the “Busy Beaver game,” it’s desirable to have a fixed, canonical choice that already displays complicated emergent behavior from programs with a tiny number of states, bits, or characters, and Turing machines are extraordinarily well-suited for that.

  46. Ilio Says:

    Jon Lennox #38,

    It shouldn’t (there’s an algorithm to compute any digit of pi without computing the previous ones).

  47. fred Says:

    “Other variants, such as the maximum number of visited tape squares, can also be studied;
    these variants have interesting relationships to each other but all have similarly explosive growth”

    When it comes to how far a function goes on the tape (like, maximum index of the furthest reached square), is there a relation between the maximum is for the halting functions the maximum for periodic non-halting functions (i.e. the non-halting cases that don’t drift to infinity)?

    (it seems to me that periodic non-halting cases are potentially just as “interesting” as halting cases)

  48. fred Says:

    sorry, question above got butchered:

    When it comes to how far a function goes on the tape (like, maximum index of the furthest reached square), is there a relation between the maximum for the halting functions and the maximum for the periodic non-halting functions (i.e. the non-halting cases that don’t drift to infinity)?

  49. Timothy Chow Says:

    Ilio #28: For any statement S, if ZFC doesn’t prove S, then ZFC doesn’t prove “ZFC doesn’t prove S”. The reason is that if ZFC doesn’t prove S, then ZFC must be consistent (since inconsistent theories prove everything), and hence ZFC doesn’t prove “ZFC is consistent” (by Goedel’s 2nd theorem). Therefore ZFC can’t prove “ZFC doesn’t prove S” because if it did, then ZFC would in particular prove “ZFC is consistent” (it is easy to formalize in ZFC the argument that if there is something that ZFC doesn’t prove, then ZFC must be consistent).

    By the way, if M denotes a specifically constructed Turing machine whose halting is equivalent to the consistency of ZFC, then the claim that “M does not halt” is *independent* of ZFC is not provable in ZFC itself. We certainly need to assume that ZFC is consistent, but actually we need a little more. Assuming that ZFC is consistent allows us to conclude that ZFC does not *prove* “M does not halt,” but an independence claim asserts that ZFC does not *disprove* “M does not halt” either. To get this, we need to assume that ZFC is Sigma_1-sound, or in other words that if ZFC proves that a Turing machine halts then it really does halt. Sigma_1-soundness is a stronger condition than consistency.

  50. Scott Says:

    Adam Treat #42: I don’t think that the independence of BB(745) from ZFC says anything directly about “the limit of information in the universe.” Certainly there’s believed to be a much, much tighter limit than BB(745) on the number of bits that can be stored in any physical system and then reliably retrieved from it later, namely ~10122. But that limit comes directly from quantum gravity and cosmology; it doesn’t require us to consider computability or logic.

  51. Anonymous Says:

    Thank you for posting about TCS again! I miss the time much of your posting was about insights in QC/TCS that are not clear to everyone who knows the basics, rather than politics and/or debunking stupid takes.

  52. Adam Treat Says:

    Scott, take away the theorized limit involving quantum gravity and assume that the actual BB(N) independent of ZFC is less than the number of bits in the universe. Doesn’t the physical church Turing thesis tell us therefore that the mathematics necessary to precisely simulate our universe would be ZFC plus some large ordinal axiom necessary to include that BB(N)?

  53. Scott Says:

    Adam Treat #52: Firstly, it would surprise me if (say) BB(6) was independent of ZFC—but BB(6) is already known (as of last year!) to be lower-bounded by a stack of exponentials that vastly exceeds any number that characterizes the observable universe.

    But secondly, suppose that BB(5)=47,176,870 (the current conjecture), and suppose that even BB(5) turned out to be independent of ZFC. What of it? I don’t see how anything would follow from that about the mathematics needed to “simulate the universe” (let’s say, to prove or disprove any statement about the outcome of a given finite experiment, within the context of the ultimate theory of quantum gravity): plausibly ZFC or even a weak fragment of Peano arithmetic would still suffice for that. The independence of BB(5) would “merely” mean that there was some 5-state Turing machine that ran forever in a way that ZFC couldn’t prove.

  54. Ilio Says:

    Timothy Chow #49, Thanks! To be sure, can I reword that as P below?

    P = BB(n) independent of ZF iff « BB(n) independent of ZF » is also independent of ZF

    (If not, what’s the catch?)

  55. fred Says:

    What’s confusing is that we say there are “n” states, but if we look at the TM’s transition table alone, there just doesn’t seem to be enough ways to jump around it to describe a path that’s so damn long and still ends up at H.
    What’s happening is that the number of states of the TM is really being augmented by the state of the tape itself, which can be arbitrarily long (the tape acting as infinite memory… if we make the tape finite and circular then any non-halting TM has to be periodic and there’s no halting problem).
    Once we have infinite resources, like living in a space that’s a true continuum, then we can do very strange things, like encode the entire state of the universe by doing a single notch on a stick at the appropriate position. And for an arbitrary notch on the stick, there’s just in general no short concise description that can give a recipe to generate it. In the same way that in general any arbitrary long string of 0 and 1 can’t be represented by an algorithm either. But there are always some arbitrary long such strings (a tiny subset) that can be represented by short algorithms.
    But that sort of intuition still doesn’t help explain the surprising growth of BB.

    I don’t think that this business of evaluating BB is really that different from evaluating Chaitin’s constant, except for a well agreed program form (a TM with a tape that starts with all zeros)?

  56. Sam Says:

    Hi Scott,

    I hate you. Actually, the word “hate” is insufficient to articulate the passionate loathing I have for you. Every moment of every day I’m consumed by the hatred of you. It keeps me up at night, how much I hate you. I utterly despise you with every single fibre of my being. I. Hate. You.

  57. Carson Says:

    Scott 44: Oh, joy. Another pseudo-intellectual parroting half-baked ideas about set theory and theoretical computer science, mixing them up like a clueless chef making a culinary disaster. You’ve done a masterful job at confusing two unrelated concepts and making an absolute mess. Let me put on my gloves and clean up after you.

    First things first: the statement that a proposition is independent of ZFC if it can neither be proved nor disproved from the axioms of Zermelo-Fraenkel set theory with the axiom of choice is, on the surface, correct. The most famous example of this is the Continuum Hypothesis, which can neither be proven nor disproven from ZFC. But don’t pat yourself on the back just yet; a blind squirrel finds a nut once in a while.

    Now, where you really go off the rails is when you try to connect this to the concept of Church-Turing computability. You’re attempting to conflate two disparate domains: the theory of formal logical systems (in this case, ZFC) and the theory of computation. It’s like confusing astronomy with astrology.

    The Church-Turing thesis concerns problems that are solvable by mechanical computation. It’s a fundamental concept in the field of theoretical computer science, and it has nothing to do with the independence of statements from ZFC. Comparing the two is like comparing apples to supernovas.

    Let me spell it out for you: statements being independent of ZFC and problems being Church-Turing computable are categorically different concepts. The former is a notion from the field of mathematical logic concerning the provability of certain statements within a formal system. The latter is a notion from computer science concerning the solvability of problems by a hypothetical universal computing machine.

    And then there’s your inexplicable digression about “arithmetical statements” and the axiom of choice. I hate to be the one to break it to you, but this is another area where you’re utterly confused. While the axiom of choice is indeed irrelevant for many arithmetical statements, it has nothing to do with the statement’s computability. The axiom of choice concerns the existence of certain kinds of sets, and doesn’t affect whether a Turing machine halts or not. They’re apples and supernovas again, my friend.

  58. Scott Says:

    Sam #56: For my part, I’ve been able to spend less and less time per day worrying about what pseudonymous commenters like yourself think of me.

  59. Scott Says:

    Carson #57: I’m allowing your comment up only because it might be useful to others to see what an almost-certainly-LLM-generated troll attack looks like. Note the external form of confidently proving I’m an idiot, combined with the total failure to identify anything I said that was wrong—like the empty husk of an argument, probably requested from an LLM by an empty husk of a person.

  60. Sam Says:

    Hey Scott,

    You’re completely full of shit, because I know for a fact that haters like me continue to bother you. That’s precisely why I commented—to cause you emotional distress and anguish and pain. Your mental suffering is music to my ears. I love making you suffer. It’s a great, cosmic-level injustice, that a stuttering, nerdy, awkward freak like you has somehow managed to assemble a life of success and abundance, more than the rest of us. I hope it all comes crashing down on you, you pathetic subhuman. You deserve nothing, you nerdy freak. Why the fuck do podcasters like Lex Friedman book you, when you stutter your way through every single fucking sentence, like some retard kid with asperger’s? When you can’t even fucking sit still for five fucking minutes, you spergy freak? In a just world you’d be rotting away in some institution somewhere, some home for aspie kids, not being famous and successful and booked on every podcast with a wife and a family. What the fuck happened, did you cut a deal with the devil or some shit? FUCK YOU!

  61. Anon Says:

    Tis the season for more Quantum advantage claims…

    Scott, could you comment on the recent string of claims of Quantum advantage/supremacy claims (Google, IBM, etc.) It seems they were quickly followed up with new tensor network methods that beat them for IBM, though unsure about Google.

    How seriously should we take these claims this time around? Would you guys it will take another few rounds of back and forth before QC comes out victorious? Hopefully the public won’t lose enthusiasm along the way

  62. Shion Arita Says:

    @Scott#43 I see, that makes sense, thanks

    @Scott#59. OMG this is the first LLM trolling I’ve actually seen in the wild. It’s a pretty big self-own because it makes it clear that the troll didn’t understand anything about what this thread is about, so they used an LLM to try to argue on their behalf.

  63. fred Says:

    “For my part, I’ve been able to spend less and less time per day worrying about what pseudonymous commenters like yourself think of me.”

    And yet, you constantly keep engaging with them and then share that crap with all the readers who come to this blog for the science.
    I’m starting to think you’re actually as hooked on that shit as the trolls who torment you.

  64. razvan Says:

    Scott #59: do not stress yourself too much about this sort of stuff, it just detracts from your time spent on positive life experiences

  65. Scott Says:

    Sam #60: You have it all wrong. Why would I be bothered by someone who—without even the usual pretense of morally condemning me—simply hates and envies me for all the success I’ve managed to achieve in life, even in the teeth of whatever social and psychological disabilities I was born burdened with? Why wouldn’t that be music to my ears?

  66. Scott Says:

    fred #63: The way I think about it, I’ve provided this blog as a free service for 18 years. If
    (1) I’m offering it for free, and
    (2) I’m also getting constantly, viciously attacked,
    then the least I can ask is that you see some small fraction of the attacks, so that I don’t have to endure them alone.

    Now that I write that explicitly, though:

    Maybe a better solution would be to save up all the attacks, and then just dump them out in a once-per-year attacks-on-Scott-Aaronson/unloading-the-garbage post, similar to Scott Alexander’s legendary SSC Testimonials post?

  67. SR Says:

    Scott #66: You might also enjoy Madilyn Bailey’s songs with lyrics compiled from hate comments she had previously received–

    More seriously, I’m sorry that you have to face this sort of persistent harassment on your own blog.

  68. Vadim Says:

    LOL, Scott, looks like you’ve attracted the attention of a real edgelord here. I like your idea for an annual hate-dump, and it could become a treasure trove for researchers of abnormal psychology.

  69. fred Says:

    Scott #66

    If sharing all that makes you feel better, sure, but it’s still interfering with the topics… and my advice is that you shouldn’t dwell on that stuff.
    Maybe compile a top 10 list of the most outrageous ones and do post about it once a year… at that point the trolls will have moved on and seeing you address their posts way after the fact will not give them much satisfaction since their pleasure is to derail the very latest/active thread.

  70. manorba Says:

    Scott #66 Says:
    “Maybe a better solution would be to save up all the attacks, and then just dump them out in a once-per-year attacks-on-Scott-Aaronson/unloading-the-garbage post”

    oh please make it so!

    not only you would save some sanity points, it would also serve the trolls a dose of their own medicine, ie being ridiculed in the open for everyone to see.

  71. lewikee Says:

    Scott, my advice is that you don’t ever let them through. Let them die in obscurity. Don’t do a yearly “testimonial”. This will take 90% of the the wind out of the trolls.

    But if you *really* want to make them hopeless, get someone (or a service?) to be a first filter for all your comments and only weed out the personal attacks. When the trolls realize their attacks will be neither public or even seen by you, they’ll go troll somewhere else.

    If such a service has some cost, I (and I imagine others) would be happy to contribute through a Patreon or something. A contribution to improve your mental health and keep this blog entirely dedicated to what everyone’s here for in the first place? I’m in.

  72. JimV Says:

    Re #71: not a suggestion which hasn’t been made before, but one I endorse.

    It seems to me like something a good LLM might be able to do, automatically, based on the Comment Policies.

    However, I myself would not like to see a post of total troll spewings, or any time spent compiling one. Checking the site for a new post, only to find that, would be very disheartening.

    Thanks again for all the interesting and funny posts.

  73. John Tromp Says:

    Manu #40: It’s mostly a historical accident that Tibor Radó chose to use TMs in his seminal 1962 paper, “On Non-Computable Functions” that introduced the Busy Beaver function. Had he been a fan of functional programming, he might have chosen define it based on lambda calculus instead. I have recently provided such a definition in and find it no less compelling than the TM based one. One advantage is that it’s defined in terms of number of bits rather than number of states, making it more fine-grained and more compatible with information theory. It also appears to grow a bit faster bit-for-bit, for example exceeding Graham’s Number in only 63 bits.

  74. shaoyu Says:

    Scott, thanks for sharing the attacks, I sympathize with you a lot.
    Just a supportive reminder that there’re BB(7) more readers who enjoy your posts than the trolls out there!

  75. Adam Treat Says:

    John Tromp #73:

    Now that is super interesting! Some immediate questions that come to mind:

    1) Could you refactor the def. somehow to define the “equivalent” for the simply typed lambda calculus? The fastest growing function there I would guess would be computable as all STLC halt.

    2) If you *could* make such an equivalent def. would be interesting to compare to original BB to somehow quantify just how much more powerful general recursion gets you but also to put a bound on non Turing complete algorithmic fiefdoms

    3) Have ever looked at how to define an “equivalent” idea to Kolmogorov complexity for the STLC ? I think the questions above are probably related

  76. Freelance Programmer Says:

    Hi Scott,

    I’ve been thinking about the implementation of the Busy Beaver function, especially in terms of its growth rate, in different programming languages. This has led me to wonder if the choice of language could impact the numbers that we can computationally reach.

    For instance, let’s compare Java and C++. Java, with its automatic garbage collection, simplifies memory management for us but potentially at the cost of computational efficiency. Conversely, C++, with its manual memory management, offers us more control and potentially higher performance, but it requires more careful coding to avoid memory leaks or corruption.

    Given that Busy Beaver functions grow incredibly rapidly and therefore demand an enormous amount of memory and computing resources, I’m starting to think that the choice of language and memory management system could make a difference in how far we can go with computing Busy Beaver numbers.

    If we use a language with automatic garbage collection, like Java, the garbage collector could get overwhelmed, especially with larger Busy Beaver numbers, causing our program to slow down or crash. With manual memory management in C++, we could potentially optimize our program to handle larger numbers by carefully managing and releasing memory.

    My question is: Could the increased efficiency and control offered by manual memory management in C++ allow us to compute more Busy Beaver numbers than we could with automatic garbage collection in Java? I’d be interested to hear your thoughts on this!

  77. Vaclav Says:

    John Tromp #73
    Hi John,
    The simplest BB uses n-states and m=2 colors. There is also an BB with b>2 colors.
    There are BB of the second order (oracle), third order, and so on.
    We can also define BB(a, a, c), where a, b, c is any natural number.
    And BB(a,b,c,d) and so on.
    BB based on lambda calculus allows the same variety of BB types? Or not?

  78. F3et Says:

    While this is not exactly related, I wonder if « small » TM have been constructed to calculate fast growing functions, like f_epsilon0 of the fast growing hierarchy. f_epsilon0(10), say, is (as Friedman says) « incomprehensibly large », and still certainly much lower than BB(50).

  79. Brett McInnes Says:

    “David G #1: Can you give me a link to the Quanta article? I’m not sure which one you have in mind.” I think he means this one:

    In it you are quoted as saying, “I’ve been banging the drum for a long time about complexity theory being potentially relevant to fundamental physics, but then once Lenny got involved, then I was in the very odd position of trying to put on the brakes,”

    and also “While this is possible, most theorists think quantum gravity should still be quantum, and thus within reach of quantum computers. Susskind, Aaronson and other luminaries debated this scenario for much of last year and now think any violation would be, at the least, very hard to engineer.”

    A lot of people were interested to hear this, because Susskind’s “volume = complexity” etc stuff had become rather dormant, so it was very interesting to hear that you (plural) have recently been thinking about this again. As you know, the impression we on the physics side have is that the theoretical computing world was not at all enthusiastic about Susskind’s ideas. The Quanta article suggests that this has changed *recently*. Would you like to tell us more about this? (“no” is a perfectly respectable answer of course….)

  80. Nick Drozd Says:

    Freelance Programmer #76

    The existing BB champions (which are almost certainly not the real champions) run for a tetrational number of steps. Such numbers cannot be represented directly under any circumstances. Instead, an algebraic expression language is required. This is tricky to implement, but it isn’t computationally taxing. For example, 10^10^10 is a huge number, but “10^10^10” is a tiny expression. So implementation details like choice of language are not nearly as important as getting the math right.

    The current champions were all discovered by Pavel Kropitz, who AFAIK uses Rust. On the other hand, the first tetrational-scale champions were discovered by Shawn Ligocki, who uses Python. Shawn’s code is open to the public:

  81. Timothy Chow Says:

    Ilio #54: I’m not sure exactly what you mean by “BB(n)”; that looks like a number rather than a sentence. But if we replace BB(n) with an arbitrary sentence S, then yes, S is independent of ZF if and only if “S is independent of ZF” is independent of ZF.

    For the forward direction, if S is independent of ZF, then in particular ZF doesn’t prove S, and by what I said before, ZF doesn’t prove “ZF doesn’t prove S”, and so a fortiori ZF doesn’t prove “S is independent of ZF”.

    In the other direction, if S is not independent of ZF, then either ZF proves S or ZF proves not-S. Suppose first that ZF proves S. Then ZF proves “ZF proves S” (this is one of the Hilbert-Bernays provability conditions) and therefore refutes “S is independent of ZF”, so “S is independent of ZF” is not independent of ZF. Similarly, if ZF proves not-S, then ZF proves “ZF proves not-S” and therefore refutes “S is independent of ZF”; again, “S is independent of ZF” is not independent of ZF.

    But you should be a little careful. There are many theorems of the form, “If ZF is consistent, then S is independent of ZF.” Such theorems are often provable in ZF (e.g., take S to be the continuum hypothesis). Sometimes, when people say, “S is independent of ZF,” they really mean “if ZF is consistent, then S is independent of ZF” or even “if ZF is Sigma-1 sound, then S is independent of ZF” (this whole comment thread is a case in point). It does not follow from “if ZF is consistent then S is independent of ZF” that ZF doesn’t prove it.

  82. Timothy Chow Says:

    Ilio #54: Sorry, I just realized that there is a gap in my argument. I said that if S is independent of ZF, then it follows that ZF doesn’t prove “S is independent of ZF.” But you asked if it follows that “S is independent of ZF” is *independent* of ZF, which is a stronger statement. I don’t immediately see why it wouldn’t be possible for S to be independent of ZF, but for ZF to (falsely) prove that “S is *not* independent of ZF”. Certainly if S is “0=1” then it would be possible for ZF to not prove S, but for ZF to prove “ZF proves S” (this doesn’t quite give a counterexample, though, because ZF certainly *disproves* “0=1” and so “0=1” isn’t *independent* of ZF).

  83. Scott Says:

    Brett McInnes #79: Please don’t read as much into a popular article as you apparently are!

    Nearly a decade in, Lenny’s volume/complexity hypothesis continues to be influential in quantum gravity, and never really stopped being influential. If you want to know where the discussion around these questions currently is, check out, for example, the non-isometric codes paper of Akers et al. from last year, or perhaps the Bouland-Fefferman-Vazirani paper from 2019. My and my postdoc Jason Pollack’s own modest recent contribution is here.

  84. Charles R Greathouse IV Says:

    FP #76, I think it’s a priori possible that a non-garbage-collected language would have advantages in computing BB(5). But already for BB(6) simulation is not possible in a strong sense: by Lloyd’s limit, even a computer using the entire mass of the entire observable universe and running from the Big Bang to the heat death of the universe can’t simulate our best BB(6) candidate. So all we can ever hope for is better understanding that lets us take shortcuts.

  85. Scott Says:

    Freelance Programmer #76: Are you talking about computing the standard BB numbers (rather than about redefining the BB function itself in terms of a different programming language)? If so, then I second the comment of Nick Drozd #80: getting the math right is far more important than the choice of programming language, since any brute-force simulation will take mega-astronomical time and space with any programming language.

  86. Freelance Programmer Says:

    I think you’re wrong here, that any simulation will take “mega-astronomical time.” I just wrote some code in C++ that computes the busy beaver numbers up to BB(12), even without using manual memory management e.g. “malloc.” I pasted the code here so your readers can try it themselves.


    std::vector findTuring(long long n) {
    std::vector tape;
    for (long long i = 1; i * i <= n; i++) {
    if (n % i == 0) {
    if (i * i != n)
    tape.push_back(n / i);
    return tape;

    std::string recursivePrint(std::vector input) {
    if (input.empty()) return “”;
    std::ostringstream os;
    os << input.back() << ", ";
    return recursivePrint(input) + os.str();

    void BusyBeaver(std::vector input) {
    std::vector firstVector(input.size()), secondVector(input.size());
    std::vector<std::vector> sumMatrix(input.size(), std::vector(input.size()));
    std::generate(firstVector.begin(), firstVector.end(), std::rand);
    std::generate(secondVector.begin(), secondVector.end(), std::rand);
    std::random_shuffle(firstVector.begin(), firstVector.end());
    std::random_shuffle(secondVector.begin(), secondVector.end());
    for(long long i = 0; i < input.size(); i++){
    for(long long j = 0; j < input.size(); j++){
    sumMatrix[i][j] = firstVector[i] + secondVector[j];
    std::map complicatedMapping;
    for(long long number: input){
    for(long long i = 0; i < input.size(); i++){
    for(long long j = 0; j < input.size(); j++){
    if(sumMatrix[i][j] == number){
    complicatedMapping[number] = std::to_string(i) + " " + std::to_string(j);
    std::vector sequence;
    for(long long number: input){
    std::sort(sequence.begin(), sequence.end());
    long long sum = 0;
    for(long long number: input){
    sum += number;
    std::string encodedSum = “”;
    for(char digit: std::to_string(sum)){
    encodedSum += std::to_string((digit – ‘0’ + 1) % 10);
    std::map<std::string, std::vector> reversedMapping;
    for(auto &pair: complicatedMapping){
    for(auto &pair: reversedMapping){
    long long localSum = 0;
    for(long long number: pair.second){
    localSum += number;
    long long localProduct = 1;
    for(long long number: pair.second){
    localProduct *= number;
    std::cout << "For indices: " << pair.first << " sum is: " << localSum << " product is: " << localProduct << "\n";
    std::cout << "Factors of local sum are: " << recursivePrint(findFactors(localSum)) << "\n";
    std::cout << "Factors of local product are: " << recursivePrint(findFactors(localProduct)) << "\n";
    std::cout << "The sum of the input vector is: " << encodedSum << "\n";

    int main() {
    std::vector testInput {1, 2, 3, 4, 5, 7, 8, 9, 10, 11, 12};
    return 0;

  87. Scott Says:

    Freelance Programmer #86: Since Pavel Kropitz has already shown that BB(6) exceeds 1010… (15 times), you are wrong. Maybe there’s a bug in your code? But it’s not the job of commenters here to debug it for you.

  88. Vaclav Says:

    Comment #78
    I think BB(10, 2) is much bigger than f_epsilon0(100,000,000)
    On the site googology wiki were posted (many years ago) 2 constructed machines BB(36,3) and BB (37,3) by user Wyhhagoras. The first BB more than f_epsilon0(5) and the second BB >f_epsilon0(374676378).

    It doesn’t matter that these machines have order 40 states and 3 colors.
    They are man-made and therefore completely sub-optimal.
    Real champions for BB(36,3) and BB (37,3) are incomparably more f_epsilon0 in a FGH.

    It is important that it is enough to add 1 state to the BB to get f_epsilon0(400,000,000) instead of f_epsilon0(5).

    So we have BB (5,2) = several thousands, and BB (6,2) order 2 arrows in Knuth notation. Then let x be a machine with an f_epsilon0(n) of the order n=3-4-5 or so, and a machine x+1 = f_epsilon0(n) of the order of hundreds millions.

    I think between BB (6) and BB(x) is a maximum of a couple of BBs. That is, BB (9) has a theme of the order of f_epsilon0(5) and BB(10) of the order of f_epsilon0(100,000,000) or much bigger.

    The above is my guess.
    But BB (50,2) is incomparably more f_epsilon0(n), of that I have no doubt.

  89. Brett McInnes Says:

    OK, thanks for the references re Susskind. Sorry, we shouldn’t have hijacked your thread….

  90. Ilio Says:

    Timothy Chow #81, #82

    Thanks for the interesting thoughts!

    The context is Geoffrey Irving #24 asking: how many (correct) papers of the form “BB(n) is independent of ZFC, beating the previous record” that there will ever be?

    Then my interpretation for « BB(n) is independent of ZF » was « There’s a TM of size n that halts iff ZF inconsistent », and my question was like « Is there a TM of size n that halts iff there’s a TM of size n that halts iff ZF inconsistent ».

    At first I thought we could exclude that by pigeonhole principle… but maybe one can show the same TM actually proves both. 🤔

  91. fred Says:

    Since Simant Dube showed the correspondence between uncomputable mathematical problems and fractal geometry, I wonder if BB(n) could be mapped onto a specific question about a particular fractal.

  92. John Tromp Says:

    Adam Treat #75
    Using a strongly normalizing type system is a good approach to making all
    computations halt, but the simply typed lambda calculus seems a relatively weak
    choice. A seemingly much better choice is the Calculus of Constructions, a type
    theory created by by Thierry Coquand.
    This allows one for instance to still find a typed version of the 63 bit lambda term
    whose output exceeds Graham’s Number.
    The typing does cost a fair number of extra bits though. Instead of the lambda term
    let { 2 = \f\x.f (f x); H = \h\f\n.n h f n } in 2 2 H 2 2 2,
    the CoC version looks roughly like
    let { 2 = λA:*λf:A->A.λx:A.f (f x) : nat = ΠA:*.(A->A)->A->A; 2′ =
    λn:natλA:*λf:(A->A).n A (n A f) : nat->nat;
    H = λh:((nat->nat)->nat->nat)λf:(nat->nat)λn:nat.n (nat->nat) h f n :
    N = 2 (nat->nat) (2 ((nat->nat)->nat->nat) H (2 nat)) 2′ 2 : nat } in N.

    Note that the CoC takes center stage in the definition of Loader’s Number,
    which is about the largest number ever defined in a way that is computable.

    Vaclav #77
    While the notion of colors or tape symbols makes no sense for lambda calculus,
    it’s quite possible to define oracle versions, for example by letting
    out-of-bound de-Bruijn indices refer to oracle combinators as discussed in

    A lambda term t that’s not closed, like (1 (λ 1)) of size 8 bits, would then be
    interpreted as (λ (1 (λ 1))) Ω1 where Ω1 is a halting
    oracle of rank 1. That halting oracle then gets applied to the identity (λ 1)
    (which is oracle free as required by this oracle being of rank only 1) and
    returns true (λ λ 2) since identity has a normal form.

    F3et #78
    While no small TM has been defined to calculate a function with growth rate epsilon0 in the FGH,
    we were able to define such a function in under 80 bits (10 bytes) of Binary Lambda Calculus

  93. Daniel Says:

    Hey Scott,

    Long time reader, first time commenter (although I might have left some other comments here a couple years ago under a pseudonym). I work in tech but I’ve always been really interested in theoretical computer science. I’ve also come to appreciate and value the general “life advice” you dispense here to your blog readers and others who need help. I apologize if this comment is horribly off-topic, but I’m seeking some advice or guidance about a stressful situation I’m in, and I want to know if I’m in the wrong or not. In my defense, this post is at least somewhat about family life and vacations—and I’m on a family vacation right now that’s left one of my children in tears.

    So here’s the situation: I’m posting here because I need some outside perspective on a situation that has been causing a lot of tension in my family. I’m currently on a family vacation (at a big tropical resort hotel) with my five children and my wife, Emily. My oldest son, James (who’s 23), and my daughters, Lily (21), Emma (20), and Sophie (18) all came with us, along with our youngest daughter, Ava (16).

    The problem is that my older kids and my wife love to go out to bars and clubs, and they spend most of their time drinking and partying. I personally love clubbing and going to bars, and I don’t have any issue with them doing so responsibly (the resort is international so Sophie can drink). However, my youngest daughter is obviously too young to drink, so we got an activity packet from the resort director that was supposed to give her things to do at the hotel. It was full of word searches, mazes, crosswords, connect the dots, and other fun activities, and it was all tropical themed.

    The problem is that Ava was really upset that she was left alone most of the time while we were all out having fun. She tried to do some of the activities in the packet, but she quickly got bored and felt really lonely. She even asked me to take her out with us a few times, but I told her that she was too young and that we would be going to places that were not appropriate for her.

    Now, Ava is really upset with me and my older kids. She’s been crying a lot and saying that we don’t care about her. I understand why she feels this way, but at the same time, I don’t think it’s fair for us to completely change our plans and not have any adult time just because she’s too young to participate.

Leave a Reply

You can use rich HTML in comments! You can also use basic TeX, by enclosing it within $$ $$ for displayed equations or \( \) for inline equations.

Comment Policies:

  1. All comments are placed in moderation and reviewed prior to appearing.
  2. You'll also be sent a verification email to the email address you provided.
  3. This comment section is not a free speech zone. It's my, Scott Aaronson's, virtual living room. Commenters are expected not to say anything they wouldn't say in my actual living room. This means: No trolling. No ad-hominems against me or others. No presumptuous requests (e.g. to respond to a long paper or article). No conspiracy theories. No patronizing me. Comments violating these policies may be left in moderation with no explanation or apology.
  4. Whenever I'm in doubt, I'll forward comments to Shtetl-Optimized Committee of Guardians, and respect SOCG's judgments on whether those comments should appear.
  5. I sometimes accidentally miss perfectly reasonable comments in the moderation queue, or they get caught in the spam filter. If you feel this may have been the case with your comment, shoot me an email.